The Theorem Prover Museum
Theorem provers are software systems that can find or check proofs for conjectures given in some logic. Research in theorem proving system started with the logical theorist 1955 and has led to a succession of systems since.
Theorem provers are complex software systems that have pushed the envelope of artificial intelligence and programming, and as such they constitute important cultural artefacts.
With the current wave of retirements of the original principal investigators there is good chance that the systems are lost, when their group servers are shut down. This web site aims to preserve the ones we can still get our hands on. This idea is compatible with the Software Heritage initiative, and contributes since it is based on GitHub repositories.
The term “museum” may be sound bit ambitious, since the exhibition and didactic interpretation of the theorem provers is beyond our scope (and perhaps abilities). But the foremost function of a museum is the conservation of artefacts, which is what the “theorem prover museum” project intends to do.
This site is the front-end to a collection of source code repositories for theorem provers (see below). Note that it is not the purpose of this site to keep the theorem proving systems running (in many cases the compilers and dependencies have moved on, making this very difficult), but only to archive the source code for academic study and aggregate meta-data about the systems. In particular this should lower the barrier of archiving systems here.
See also most wanted list, systems believed lost, active provers, how to contribute, Community, project/issues.
Latest News Full List 
- Theorem Prover Museum has 30 Provers (20 June 2018)
- Call for Theorem Prover Metadata (30 September 2017)
- Theorem Prover Museum has news (22 September 2017)
- swMATH links (9 September 2017)
- The sources of the first theorem prover (Logic Theorist) found! (2 September 2017)
Related Resources
Encyclopedia of proof systems, Wikipedia page, … more.
All theorem provers start out as active systems, eventually development gets discontinued as developers retire or move to newer systems. Therefore we also maintain a list of source code repositories of active theorem provers.
Theorem Provers
There are 43 provers in the listing below.
The IMPS Theorem Prover.
| authors: | William M. Farmer, Joshua D. Guttman, F. Javier Thayer |
|---|---|
| language: | Scheme, Common Lisp |
The Fellowship Theorem Prover
| authors: | Florent ????? |
|---|---|
| language: | ???? |
The Markgraph Karl Refutation Procedure, a graph-based resolution theorem prover
| authors: | Jörg Siekmann, Jürgen Ohlbach, Axel Präcklein |
|---|---|
| language: | Common Lisp (CLOS) |
A theorem prover for higher-order logic based on proof planning.
| authors: | Jörg Siekmann, Detlef Fehrer, Christoph Benzmüller, Michael Kohlhase, Manfred Kerber |
|---|---|
| language: | Common Lisp (CLOS) |
An Inductive Theorem Prover
| authors: | Dieter Hutter |
|---|
The first theorem prover for first-order logic with equality from the Argonne group that was widely distributed.
| authors: | William McCune |
|---|---|
| language: | C |
The Argonne Model generator.
| authors: | William McCune |
|---|---|
| language: | C |
Prover9 is the successor to Otter
| authors: | William McCune |
|---|---|
| language: | C |
Mace4 is the successor of Mace.
| authors: | William McCune |
|---|---|
| language: | C |
The Prolog Equation Solving System (PRESS) pioneered work on what is now called proof planning.
| authors: | Alan Bundy |
|---|---|
| language: | Prolog |
The original Edinburgh LCF
| authors: | Robin Milner |
|---|---|
| development: | 1972-1977 |
TPS is an interactive, semi-automatic, and automatic Theorem Proving System for first-order logic and higher-order logic.
| authors: | Peter Andreas, Frank Pfenning, Dale Miller, Sunil Issar, Hongwei Xi, Mathhew Bishop, Chad Brown |
|---|---|
| language: | Comon Lisp |
ETPS is a subsystem of TPS designed for interactive use by students in logic courses.
| authors: | Peter Andreas, Frank Pfenning, Dale Miller, Sunil Issar |
|---|---|
| language: | Common Lisp |
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.
| authors: | Mike Gordon, Tom Melham, and numerous other contributors |
|---|
The rational reconstruction of HOL88
| authors: | Konrad Slind, Graham Birtwistle |
|---|
an early theorem prover written in SNOBOL
| authors: | Wolfgang Bibel |
|---|---|
| language: | SNOBOL |
A general-purpose instance-based first-order automated theorem proving algorithm
A Semantically Guided First-Order Theorem Prover
A Prolog implementation of the proof planner Clam (in the clam2 development branch) and the associated theorem prover, oyster.
| authors: | Alan Bundy |
|---|---|
| language: | Prolog |
Prolog implementation of proof planner with critics, and some higher-order unification, in the v3 branch of Clam.
| language: | Prolog |
|---|
A proof planning system that support proof planning over higher-order domains.
A Distributed and Learning Equational Prover.
A proof checker and interactive theorem prover for dependently typed set theory.
| authors: | Chad Brown |
|---|
A first-order theorem prover based on the connection method.
| authors: | Johann Schumann, Wolfgang Bibel |
|---|
A theorem prover based on the PTTP paradigm.
| home page: | http://koralle.htwk-leipzig.de/ProCom/index.html |
|---|---|
| authors: | Gerd Neugebauer, Uwe Petermann |
| development: | 1992-1995 |
| license: | GPL V1 |
| language: | (ECLiPSe) Prolog |
The first theorem prover by Newell and Simon.
| authors: | Alan Newell, Herbert Simon |
|---|
| home page: | http://strictlypositive.org/samizdat.html |
|---|---|
| authors: | Conor McBride |
| language: | Standard ML and LEGO |
| Repository: | R1 |
Rewrite and Decision Procedure Laboratory
| authors: | Alessandro Armando, Luca Compagna, Silvio Ranise |
|---|---|
| license: | GPL 3.0 |
| language: | Prolog |
| Repository: | R1 |
| authors: | J Strother Moore, Robert S. Boyer (Grant O. Passmore: OCaml Reimplementation) |
|---|---|
| development: | 1972/3 |
| language: | Pure Lisp |
| note: | the code is still linked from the ACL github repository. |
The prover of the Robbins Conjecture
| home page: | http://www.cs.unm.edu/~mccune/eqp/ |
|---|---|
| wikipedia: | https://en.wikipedia.org/wiki/EQP |
| authors: | William McCune |
| language: | C |
an early interactive proof development system for various type theories
| home page: | http://www.dcs.ed.ac.uk/home/lego/ |
|---|---|
| wikipedia: | https://en.wikipedia.org/wiki/LEGO_(proof_assistant) |
| authors: | Randy Pollack |
| development: | <= 1999 |
| note: | See http://homepages.inf.ed.ac.uk/rpollack/bibfile.html for some old documents. |
Edinburgh LCF re-implemented in Standard ML
| authors: | Konrad Slind |
|---|---|
| development: | 1980-1985 |
| language: | Standard ML |
a Clause-Diffusion parallelization of Otter 2.2 for workstation networks
| home page: | http://profs.sci.univr.it/~bonacina/cdprovers.html |
|---|---|
| authors: | Maria Paola Bonacina |
| development: | 1992 - 1992 |
| language: | C, PCN |
a Clause-Diffusion prover parallelizing Otter Parts Store code for equational theories (modulo AC)
| home page: | http://profs.sci.univr.it/~bonacina/cdprovers.html |
|---|---|
| authors: | Maria Paola Bonacina, William W. McCune |
| development: | 1993 - 1995 |
| language: | C, p4 |
a Modified-Clause-Diffusion prover parallelizing Otter Parts Store code for equational theories (modulo AC)
| home page: | http://profs.sci.univr.it/~bonacina/cdprovers.html |
|---|---|
| authors: | Maria Paola Bonacina |
| development: | 1995 - 1996 |
| language: | C, p4 |
a Modified-Clause-Diffusion parallelization of EQP 0.9 for either workstation networks or multi-processors
| home page: | http://profs.sci.univr.it/~bonacina/cdprovers.html |
|---|---|
| authors: | Maria Paola Bonacina |
| development: | 1996 - 1999 |
| language: | C, MPI |
a Modified-Clause-Diffusion parallelization of EQP 0.9d for workstation networks
| home page: | http://profs.sci.univr.it/~bonacina/cdprovers.html |
|---|---|
| authors: | Maria Paola Bonacina |
| development: | 1999 - 2000 |
| language: | C, MPI |
a Modified-Clause-Diffusion plus multi-search parallelization of EQP 0.9d for workstation networks
| home page: | http://profs.sci.univr.it/~bonacina/cdprovers.html |
|---|---|
| authors: | Maria Paola Bonacina, Javeed Chida |
| development: | 2000 - 2001 |
| language: | C, MPI |
Automated induction and theory exploration for Haskell programs.
| authors: | Dan Rosén, Nicholas Smallbone, Moa Johansson, Koen Claessen |
|---|---|
| development: | 2011 - 2014 |
| language: | Haskell |
| Repository: | R1 |
| note: | A sister system to Hipster, using the same backend for conjecture discovery (QuickSpec) but for Haskell programs. |
A proof planner for Isabelle/HOL focusing on automated induction.
| authors: | Lucas Dixon, Moa Johansson (+ possibly others too) |
|---|---|
| development: | approx. 2000 - 2015. |
| language: | Poly ML |
| Repository: | R1 |
| note: | The theory exploration system IsaCoSy exists in the same repo (see synthesis directory). |
For generating type-secure and efficient Lisp programs.
| home page: | https://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/lang/lisp/code/tools/sequel/0.html |
|---|---|
| authors: | Mark Tarver |
| development: | 1990-1994 |
| language: | Common Lisp |