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:
“Away with the cant of “Measures, not men!”Mthe idle supposition that it is the harness and not the horses that draw the chariot along. No, Sir, if the comparison must be made, if the distinction must be taken, men are everything, measures comparatively nothing.”
—George Canning (1770–1827)
“From top to bottom of the ladder, greed is aroused without knowing where to find ultimate foothold. Nothing can calm it, since its goal is far beyond all it can attain. Reality seems valueless by comparison with the dreams of fevered imaginations; reality is therefore abandoned.”
—Emile Durkheim (1858–1917)
“It is very important not to become hard. The artist must always have one skin too few in comparison to other people, so you feel the slightest wind.”
—Shusha Guppy (b. 1938)