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:
“The difference between human vision and the image perceived by the faceted eye of an insect may be compared with the difference between a half-tone block made with the very finest screen and the corresponding picture as represented by the very coarse screening used in common newspaper pictorial reproduction. The same comparison holds good between the way Gogol saw things and the way average readers and average writers see things.”
—Vladimir Nabokov (1899–1977)
“Intolerance respecting other people’s religion is toleration itself in comparison with intolerance respecting other people’s art.”
—Wallace Stevens (1879–1955)
“When we reflect on our past sentiments and affections, our thought is a faithful mirror, and copies its objects truly; but the colours which it employs are faint and dull, in comparison of those in which our original perceptions were clothed.”
—David Hume (1711–1776)