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:
“[Girls] study under the paralyzing idea that their acquirements cannot be brought into practical use. They may subserve the purposes of promoting individual domestic pleasure and social enjoyment in conversation, but what are they in comparison with the grand stimulation of independence and self- reliance, of the capability of contributing to the comfort and happiness of those whom they love as their own souls?”
—Sarah M. Grimke (1792–1873)
“Most parents aren’t even aware of how often they compare their children. . . . Comparisons carry the suggestion that specific conditions exist for parental love and acceptance. Thus, even when one child comes out on top in a comparison she is left feeling uneasy about the tenuousness of her position and the possibility of faring less well in the next comparison.”
—Marianne E. Neifert (20th century)
“It is comparison than makes people miserable.”
—Chinese proverb.