Comparison
See also: Proof assistant#Comparison and Category:Theorem proving software systems
| Name | License type | Web service | Library | Standalone | Version | Last update | Author | Notice |
|---|---|---|---|---|---|---|---|---|
| ACL2 | GPL v2 | No | No | Yes | 5.0 | 08/23/2012 | Matt Kaufmann, J. Strother Moore | - |
| Prover9 / Mace4 | GPLv2 | No | Yes | Yes | v05 | 11/04/2009 | William McCune / Argonne National Laboratory | - |
| Otter | Public Domain | Via System on TPTP | Yes | No | 3.3f | 09/2004 | William McCune / Argonne National Laboratory | Succeded by Prover9 / Mace4 |
| j'Imp | ? | No | No | Yes | - | 05/28/2010 | André Platzer | - |
| Metis | ? | No | Yes | No | 2.2 | 05/24/2010 | Joe Hurd | - |
| Jape | ? | Yes | Yes | No | 1.0 | 03/22/2010 | Adolfo Gustavo Neto, USP | - |
| PVS | ? | No | Yes | No | 4.2 | 07/2008 | Computer Science Laboratory of SRI International, California, USA | - |
| Leo II | ? | Via System on TPTP | Yes | Yes | 1.2.8 | 2011 | Christoph Benzmüller, Frank Theiss, Larry Paulson. FU Berlin and University of Cambridge | - |
| EQP | ? | No | Yes | No | 0.9e | May/2009 | William McCune / Argonne National Laboratory | - |
| SAD | ? | Yes | Yes | No | 2.3-2.5 | 08/27/2008 | Alexander Lyaletski, Konstantin Verchinine, Andrei Paskevich | - |
| PhoX | ? | No | Yes | No | 0.88.100524 | - | Christophe Raffalli, Philippe Curmin, Pascal Manoury, Paul Roziere | - |
| KeYmaera | GPL | Via Java Webstart | Yes | Yes | 2.1 | 05/2012 | André Platzer, Jan-David Quesel; Philipp Rümmer; David Renshaw | - |
| Gandalf | ? | No | Yes | No | 3.6 | 2009 | Matt Kaufmann e J. Strother Moore, Universidade de Texas em Austin | - |
| Tau | ? | No | Yes | No | - | 2005 | Jay R. Halcomb e Randall R. Schulz da H&S Information Systems | - |
| E | GPL | Via System on TPTP | No | Yes | E 1.4 | 08/20/2011 | Stephan Schulz, Automated Reasoning Group, Technical University of Munich | - |
| SNARK | Mozilla Public License | No | Yes | No | snark-20080805r018b | 2008 | Mark E. Stickel | - |
| Vampire | ? | Via System on TPTP | Yes | Yes | Third re-incarnation Vampire | 2011 | Andrei Voronkov, Alexandre Riazanov, Krystof Hoder | - |
| Waldmeister | ? | Yes | Yes | No | - | - | Thomas Hillenbrand, Bernd Löchner, Arnim Buch, Roland Vogt, Doris Diedrich | - |
| Saturate | ? | No | Yes | No | 2.5 | 10/1996 | Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela Pilar Nivela | - |
| Theorem Proving System (TPS) | ? | No | Yes | No | - | 06/24/2004 | Carnegie Mellon University | - |
| SPASS | ? | Yes | Yes | Yes | 3.7 | 11/2005 | Max Planck Institut Informatik | - |
| IsaPlanner | GPL | No | Yes | Yes | IsaPlanner 2 | 2007 | Lucas Dixon, Johansson Moa | - |
| KeY | GPL | Yes | Yes | Yes | 1.6 | 10/2010 | Karlsruhe Institute of Technology, Chalmers University of Technology, University of Koblenz | - |
| Theorem Checker | ? | Yes | No | No | 0 | 2010 | Robert J. Swartz, Northeastern Illinois University | - |
Read more about this topic: Automated Theorem Proving
Famous quotes containing the word comparison:
“Envy and jealousy are the private parts of the human soul. Perhaps the comparison can be extended.”
—Friedrich Nietzsche (1844–1900)
“The comparison between Coleridge and Johnson is obvious in so far as each held sway chiefly by the power of his tongue. The difference between their methods is so marked that it is tempting, but also unnecessary, to judge one to be inferior to the other. Johnson was robust, combative, and concrete; Coleridge was the opposite. The contrast was perhaps in his mind when he said of Johnson: “his bow-wow manner must have had a good deal to do with the effect produced.””
—Virginia Woolf (1882–1941)
“Intolerance respecting other people’s religion is toleration itself in comparison with intolerance respecting other people’s art.”
—Wallace Stevens (1879–1955)