theorem-prover
There are 127 repositories under theorem-prover topic.
HigherOrderCO/Kind
A modern proof language
acl2/acl2
ACL2 System and Books as Maintained by the Community
SRI-CSL/yices2
The Yices SMT Solver
johnyf/tool_lists
Links to tools by subject
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.
0vercl0k/z3-playground
A repository to store Z3-python scripts you can use as examples, reminders, whatever.
Chymyst/curryhoward
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
lukaszcz/coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
msakai/toysolver
My sandbox for experimenting with solver algorithms.
cicada-lang/cicada-solo
Cicada Language (solo version)
andrew-johnson-4/LSTS
Large Scale Type Systems (programming language)
joom/hezarfen
a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features
kovvalsky/LangPro
Tableau-based Theorem Prover for Natural Logic and Language
JetBrains-Research/coqpilot
VSCode extension that is designed to help automate writing of Coq proofs.
evhub/pyprover
Resolution theorem proving for predicate logic in pure Python.
cicada-lang/cicada-plct
Cicada Language (PLCT little team)
LS-Lab/KeYmaeraX-release
KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
philzook58/egglog0
Datalog + Egg = Good
janicicpredrag/gclc
GCLC is a mathematical software tool for producing high-quality mathematical illustrations, for teaching mathematics, and for automated proving of geometry theorems.
ai4reason/Prover9
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
lapisla-prover/lapisla-prover
lapisla is a *battery-pluggable* theorem prover and ecosystem designed for everyone. Greetings! 👋
cheuktingli/psitip
Python Symbolic Information Theoretic Inequality Prover
uuverifiers/ostrich
An SMT Solver for string constraints
joom/WangsAlgorithm
A classical propositional theorem prover in Haskell, using Wang's Algorithm.
ptarau/TypesAndProofs
Type inference algorithms and intuitionistic propositional theorem provers solving type inhabitation problems
gilith/metis
An automatic theorem prover for first order logic with equality
namin/leanTAP
A Declarative Theorem Prover for First-Order Classical Logic
uuverifiers/princess
The Princess Theorem Prover
forked-from-1kasper/anders
Anders: Cubical Type Checker
anqur/TinyLean
Tiny theorem prover with syntax like Lean 4 in <1K LOC
groupoid/anders
🧊 Модальний гомотопічний верифікатор математики
RiccardoBiosas/LeanGPT
Experiments with interactive theorem provers, LLMs and formal systems
taktoa/eqsat
A language-generic implementation of equality saturation in Haskell
nclarius/pyPL
Analytic tableau based minimal model generator, model checker and theorem prover for first-order logic with modal extensions
dominique-unruh/qrhl-tool
Proof assistant for qRHL
nilqed/SNARK
SNARK - SRI's New Automated Reasoning Kit