The Most Wanted List for the Theorem Prover Museum

The following theorem provers are not featured in the Theorem Prover Museum but are important cultural artifacts. We list the system and known associates here. There is also a list of systems believed lost.

Note that the Theorem Prover Museum wants to preserve the (stable) source code of theorem proving systems that are no longer under active development. Active systems typically have repositories of their own. We list them separately.

If you know the last authors/maintainers and please contact them and ask them to contribute the sources. To contribute source code or suggest a system for inclusion, please contact Michael Kohlhase. Alternatively, just open an issue on our tracker.

Acknowledgements: Thanks to the following colleagues for suggestions: Alan Bundy, Josef Urban, Jacques Fleuriot, Cezar Munoz, Freek Wiedijk, Jörg Siekmann, Georges Gonthier, Florian Rabe, Larry Paulson, Konrad Slind, David Plaisted, Matt Kaufmann, John Harrison, Mike Gordon, Maria Paola Bonacina.

We list theorem proving systems and their known associates (for contact) and state

There are 31 provers in the listing below.

Tatzelwurm

authors:Thomas Käufl & Nicolas Zabel
note:cannot find the authors online
Gandalf

authors:Tannel Tammet
note:contacted Tannel Tammet 2017-04-07
PTTP

authors:Mark Stickel
RRTP

authors:David Plaisted (or his students?)
note:David Plaisted promised to look for them
CLINC-S

authors:David Plaisted (or his students?)
Darwin

authors:Peter Baumgartner
note:Peter has been contacted but did not reply :-(
Scott

authors:John Slaney
many non-classical provers by Rajeev Gore

note:they are here, hoping that Rajeev will package them himself
MetaPRL

note:MetaPRL has a SVN repos, but the last commit seems 8 years old
the provers in the resolution paper by Alan Robinson

authors:Alan Robinson
LEO I

authors:Christoph Benzmüller
language:Common Lisp
Chaff

note:zChaff is at http://www.princeton.edu/~chaff/zchaff.html, maybe they know older versions as well.
Larch

authors:Stephen Garland, Guttag
note:look at Wikipedia and MMT page
Coq 1

authors:Gerard Huet
note:George Gonthier will ask him
Matita 1

authors:Claudio Sacerdoti Coen et. al.
early Mizar

authors:Andrzej Tryplec et. al.
language:Pascal
note:Adam Naumowicz will look for Mizar4
LeanTaP

authors:Bernhard Beckert
language:Prolog
AM

wikipedia:https://en.wikipedia.org/wiki/Automated_Mathematician
authors:Doug Lenat
note:there is a prolog reimplementation. Joerg Siekmann contact him repeatedly, but did not receive answer
EVES/NEVER

authors:Kromodimoeljo, Pase, Saaltink, Craigen, Meisels
note:EVES/NEVER
SAM

authors:J. R. Guard, F. C. Oglesby, J. H. Bennett, L. G. Settle;
note:does anyone have contact to them?
The conjecturing systems by Simon Colton

authors:Simon Colton
Martin Davis' Presburger implementation

authors:Martin Davis
The first Davis-Putnam

The first DPLL implementation

Early model elimination / MESON

authors:Don Loveland, Mark Stickel, ...
Dag Prawitz's early unification-based prover

authors:Dag Prawitz
Paul Gilmore's early first-order prover

authors:Paul Gilmore
note:see this for reference
Hao Wang's AE prover and full FOL prover (IBM?)

authors:Hao Wang
note: see here
ALF, and related systems

note:contacted Bengt Nordstrom 2017-04-06 and multiple afterwards
?????

authors:Chu
note:Chu (Austin) wrote a system with polynomials (J. Moore told me)
the ITP@Maude

authors:Manuel Claudel
note:author contacted 2017-09-22