theorem-prover

There are 119 repositories under theorem-prover topic.

HigherOrderCO/Kind1
A next-gen functional language
Language:Rust3.5k 75 213142
johnyf/tool_lists
Links to tools by subject
361 44 082
SRI-CSL/yices2
The Yices SMT Solver
Language:SMT357 24 37245
acl2/acl2
ACL2 System and Books as Maintained by the Community
Language:Common Lisp345 35 48296
newca12/awesome-rust-formalized-reasoning
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
279 13 09
0vercl0k/z3-playground
A repository to store Z3-python scripts you can use as examples, reminders, whatever.
Language:Python273 20 528
Chymyst/curryhoward
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
Language:Scala255 16 615
lukaszcz/coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Language:OCaml208 8 8531
msakai/toysolver
My sandbox for experimenting with solver algorithms.
Language:Haskell152 11 2211
cicada-lang/cicada-solo
Cicada Language (solo version)
Language:TypeScript125 3 65
joom/hezarfen
a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features
Language:Idris118 8 03
kovvalsky/LangPro
Tableau-based Theorem Prover for Natural Logic and Language
Language:Prolog109 8 510
andrew-johnson-4/LSTS
Large Scale Type Systems (programming language)
Language:Rust101 4 1283
cicada-lang/cicada-plct
Cicada Language (PLCT little team)
Language:TypeScript91 3 496
evhub/pyprover
Resolution theorem proving for predicate logic in pure Python.
Language:Python89 6 59
LS-Lab/KeYmaeraX-release
KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
Language:Scala72 14 11036
philzook58/egglog0
Datalog + Egg = Good
Language:Rust65 5 23
joom/WangsAlgorithm
A classical propositional theorem prover in Haskell, using Wang's Algorithm.
Language:Haskell36 4 34
cheuktingli/psitip
Python Symbolic Information Theoretic Inequality Prover
Language:Python32 7 17
ai4reason/Prover9
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
Language:C31 4 19
ptarau/TypesAndProofs
Type inference algorithms and intuitionistic propositional theorem provers solving type inhabitation problems
Language:Prolog30 1 13
uuverifiers/ostrich
An SMT Solver for string constraints
Language:Scala30 4 439
gilith/metis
An automatic theorem prover for first order logic with equality
Language:Standard ML28 1 111
namin/leanTAP
A Declarative Theorem Prover for First-Order Classical Logic
Language:Scheme25 6 02
taktoa/eqsat
A language-generic implementation of equality saturation in Haskell
Language:Haskell21 10 163
uuverifiers/princess
The Princess Theorem Prover
Language:Scala19 5 85
forked-from-1kasper/anders
Anders: Cubical Type Checker
Language:OCaml18 1 01
groupoid/anders
🧊 Модальний гомотопічний верифікатор математики
Language:OCaml18 0 03
nclarius/pyPL
Analytic tableau based minimal model generator, model checker and theorem prover for first-order logic with modal extensions
Language:Python18 0 02
dominique-unruh/qrhl-tool
Proof assistant for qRHL
Language:Scala17 5 763
RiccardoBiosas/LeanGPT
Experiments with interactive theorem provers, LLMs and formal systems
Language:Coq16 2 02
catseye/Philomath
MIRROR of https://codeberg.org/catseye/Philomath : An LCF-style theorem prover written in C89 (a.k.a ANSI C)
Language:C14 3 12
adyavanapalli/natural-number-game-solutions
Solutions to Imperial College London's Natural Number Game, a gamified formal mathematics course on the Peano axioms using an interactive + automated theorem prover developed by Microsoft Research called Lean.
11 2 06
dannypsnl/k
k theorem prover
Language:Racket11 4 421
bor0/budge
Budge - a programming language and a theorem prover
Language:Jupyter Notebook10 2 01
yakuza8/first-order-predicate-logic-theorem-prover
Autonomous Theorem Prover for First Order Predicate Logic
Language:Python10 2 03

theorem-prover

HigherOrderCO/Kind1

johnyf/tool_lists

SRI-CSL/yices2

acl2/acl2

newca12/awesome-rust-formalized-reasoning

0vercl0k/z3-playground

Chymyst/curryhoward

lukaszcz/coqhammer

msakai/toysolver

cicada-lang/cicada-solo

joom/hezarfen

kovvalsky/LangPro

andrew-johnson-4/LSTS

cicada-lang/cicada-plct

evhub/pyprover

LS-Lab/KeYmaeraX-release

philzook58/egglog0

joom/WangsAlgorithm

cheuktingli/psitip

ai4reason/Prover9

ptarau/TypesAndProofs

uuverifiers/ostrich

gilith/metis

namin/leanTAP

taktoa/eqsat

uuverifiers/princess

forked-from-1kasper/anders

groupoid/anders

nclarius/pyPL

dominique-unruh/qrhl-tool

RiccardoBiosas/LeanGPT

catseye/Philomath

adyavanapalli/natural-number-game-solutions

dannypsnl/k

bor0/budge

yakuza8/first-order-predicate-logic-theorem-prover