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:
“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)
“But the best read naturalist who lends an entire and devout attention to truth, will see that there remains much to learn of his relation to the world, and that it is not to be learned by any addition or subtraction or other comparison of known quantities, but is arrived at by untaught sallies of the spirit, by a continual self-recovery, and by entire humility.”
—Ralph Waldo Emerson (1803–1882)
“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)