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.
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)
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.
The Argonne Model generator.
|authors:||J Strother Moore, Robert S. Boyer (Grant O. Passmore: OCaml Reimplementation)|
|note:||the code is still linked from the ACL github repository.|
an early interactive proof development system for various type theories
|note:||See http://homepages.inf.ed.ac.uk/rpollack/bibfile.html for some old documents.|
Edinburgh LCF re-implemented in Standard ML