The Theorem Prover Museum: Active Provers
All theorem provers start out as active systems, eventually development gets discontinued as developers retire or move to newer systems.
Therefore the Theorem Prover Museum maintains a list of source code repositories of active theorem provers as well, hoping that they will prosper for a long time.
This list also contains theorem provers that many assume not to be active anymore. Some of the systems get here when I contact the maintainers to donate the code for the museum. For instance, I contacted David McAllester (who had not been seen in the ATP community for a decade) about the Ontic theorem prover and I got the somewhat indignant reply … but Ontic lives!!!!. pro
There are 10 provers in the listing below.
An automatic theorem proving system using knowledge and metaknowledge in mathematics.
| home page: | http://www.normalesup.org/~pastre/muscadet/muscadet.html |
|---|---|
| authors: | Dominique Pastre |
| development: | 1984- |
| license: | BSD |
| language: | Prolog |
A Generic Theorem Prover
| home page: | https://isabelle.in.tum.de |
|---|---|
| wikipedia: | https://en.wikipedia.org/wiki/Isabelle_(proof_assistant) |
| authors: | Tobias Nipkow, Lawrence Paulson, Makarius Wenzel and numerous others |
| development: | 1985- |
| license: | BSD |
| language: | Standard ML and Scala |
| Repository: | R1 |
to come soon
| authors: | David McAllister et al. |
|---|
| authors: | Bob Constable, Christoph Kreitz, et. al. |
|---|---|
| note: | still being used, but maintained? |
| home page: | http://class-int.narod.ru/ |
|---|---|
| authors: | Oleg Okhotnikov, Yuri Vtorushin |
| development: | 2004-2007 |
| language: | C++ |
| note: | This is an early variant of our system, which we used in practical classes at the university; we plan to resume development in the near future |
Automated induction and theory exploration on top of Isabelle/HOL.
| authors: | Moa Johansson, Irene Lobo Valbuena, Solrun Halla Einarsdottir, Johannes Åman Pohjola |
|---|---|
| development: | 2014 - |
| language: | PolyML (Haskell) |
| Repository: | R1 |
| note: | A sister system and successor of HipSpec, using the same backend for conjecture discovery (QuickSpec) but for Isabelle/HOL theories. |
Continuation of SAD at the University of Bonn.
| home page: | https://naproche.github.io/ |
|---|---|
| authors: | Andrei Paskevich, Steffen Frerix, Makarius Wenzel, Anton Lorenzen, Adrian Marti, and others |
| maintainers: | Logic group at the University of Bonn |
| development: | 2018- |
| license: | GPL 3.0 |
| language: | Haskell, Scala, ML |
| Repository: | R1 |
Why3 is a platform for deductive program verification.
| home page: | http://why3.lri.fr/ |
|---|---|
| authors: | Claude Marche, Guillaume Melquiond, Sylvain Dailler, Benedikt Becker, Raphael Rieu-Helft, Jean-Christophe Filliatre, Cláudio Belo Lourenço, Andrei Paskevich, Mário Pereira, and others |
| maintainers: | Toccata (at INRIA) |
| development: | 2007- |
| license: | GPL 2.1 |
| language: | OCaml, Coq |
| Repository: | R1 |
Interactive theorem proving for students.
| home page: | https://elfe-prover.org/ |
|---|---|
| authors: | Maximilian Doré |
| development: | 2017-2018 |
| license: | MIT |
| language: | Haskell, JavaScript |
| Repository: | R1 |