Pinned Repositories
clam3
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.
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.
imps
The IMPS Theorem Prover
LCF77
The original Edinburgh LCF.
logic-theorist
The sources of the first theorem prover.
OMEGA
A theorem prover for higher-order logic based on proof planning.
otter
The first theorem prover and model generator for first-order logic with equality from the Argonne group that was widely distributed.
prover9
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
theoremprover-museum.github.io
theoremprover-museum's Repositories
theoremprover-museum/logic-theorist
The sources of the first theorem prover.
theoremprover-museum/theoremprover-museum.github.io
theoremprover-museum/prover9
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
theoremprover-museum/clam3
Prolog implementation of proof planner with critics, and some higher-order unification, in the v3 branch of Clam.
theoremprover-museum/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.
theoremprover-museum/HOL90
The source of hte HOL90 Theorem prover.
theoremprover-museum/SETHEO
The SETHEO theorem prover (C version)
theoremprover-museum/egal
Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory
theoremprover-museum/lambdaclam
theoremprover-museum/LEGO
the source archive for LEGO: an interactive proof development system for various type theories
theoremprover-museum/muscadet
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.
theoremprover-museum/scunac
a proof checker and interactive theorem prover for dependently typed set theory
theoremprover-museum/doc
Documentation about the Theorem Prover Museum
theoremprover-museum/oleg
theoremprover-museum/ProCom
A theorem prover based on the PTTP paradigm.
theoremprover-museum/SNARK
SNARK - SRI's New Automated Reasoning Kit
theoremprover-museum/Aquarius
The Aquarius Theorem Prover
theoremprover-museum/ClassInt
theoremprover-museum/discount
the discount theorem prover
theoremprover-museum/Ehdm
The Ehdm theorem prover developed at SRI in the 80s.
theoremprover-museum/fellowship
theoremprover-museum/isabelle
Archival Versions of the Isabelle Theorem Prover
theoremprover-museum/larch
The Larch Theorem Prover from MIT
theoremprover-museum/minlog
theoremprover-museum/OSHL
theoremprover-museum/Peers
The Peers Theorem Prover
theoremprover-museum/Peers-mcd
the Peers-mcd theorem provers
theoremprover-museum/PLTP
The Edinburgh Pure Lisp Theorem Prover (Boyer/Moore)
theoremprover-museum/RDL
Rewrite and Decision Procedure Laboratory
theoremprover-museum/SEQUEL
Mark Tarver's SEQUEL system versions 7.0 and 5.3