There are no reviews yet. Be the first to send feedback to the community and the maintainers!
logic-theorist
The sources of the first theorem prover.theoremprover-museum.github.io
LCF77
The original Edinburgh LCF.prover9
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.HOL88
The HOL System is an environment for interactive theorem proving in a higher-order logic. Its most outstanding feature is its high degree of programmability through the meta-language ML.OMEGA
A theorem prover for higher-order logic based on proof planning.imps
The IMPS Theorem Proverclam3
Prolog implementation of proof planner with critics, and some higher-order unification, in the v3 branch of Clam.EQP
EQP is an automated theorem proving program for first-order equational logic. Its strengths are good implementations of associative-commutative unification and matching, a variety of strategies for equational reasoning, and fast search.InKa
InKa - an inductive theorem proverotter
The first theorem prover and model generator for first-order logic with equality from the Argonne group that was widely distributed.HOL90
The source of hte HOL90 Theorem prover.MKRP
The Markgraph Karl Refutation Procedure, a graph-based resolution theorem prover written in Common LispSETHEO
The SETHEO theorem prover (C version)TPS
TPS is an interactive, semi-automatic, and automatic Theorem Proving System for first-order logic and higher-order logic. The subsystem ETPS is designed for interactive use by students in logic courses.LEGO
the source archive for LEGO: an interactive proof development system for various type theoriesscunac
a proof checker and interactive theorem prover for dependently typed set theorylambdaclam
egal
Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theorySNARK
SNARK - SRI's New Automated Reasoning KitProCom
A theorem prover based on the PTTP paradigm.doc
Documentation about the Theorem Prover Museumoleg
clam2
A Prolog implementation of the proof planner Clam (in the clam2 development branch) and the associated theorem prover, oyster.Love Open Source and this site? Check out how you can help us