There are no reviews yet. Be the first to send feedback to the community and the maintainers!
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 theorymuscadet
The Muscadet Theorem Prover is a knowledge-based system. Based on natural deduction, it uses methods which resemble those used by humans, implemented in one or several bases of facts. The output is an easily readable proof.SNARK
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