Automated Theorem Proving - Comparison

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:

    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 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)

    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)