World Library  
Flag as Inappropriate
Email this Article

Automated theorem prover

Article Id: WHEBN0001531203
Reproduction Date:

Title: Automated theorem prover  
Author: World Heritage Encyclopedia
Language: English
Subject: Lambda calculus, Specification language, Formal methods, Theorem prover, ACL2, QED manifesto, Domain-specific language, ESC/Java, Superposition calculus, Term indexing
Collection:
Publisher: World Heritage Encyclopedia
Publication
Date:
 

Automated theorem prover

Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

Logical foundations

While the roots of formalised logic go back to Aristotle, the end of the 19th and early 20th centuries saw the development of modern logic and formalised mathematics. Frege's Begriffsschrift (1879) introduced both a complete propositional calculus and what is essentially modern predicate logic.[1] His Foundations of Arithmetic, published 1884,[2] expressed (parts of) mathematics in formal logic. This approach was continued by Russell and Whitehead in their influential Principia Mathematica, first published 1910-1913,[3] and with a revised second edition in 1927.[4] Russell and Whitehead thought they could derive all mathematical truth using axioms and inference rules of formal logic, in principle opening up the process to automatisation. In 1920, Thoralf Skolem simplified a previous result by Leopold Löwenheim, leading to the Löwenheim–Skolem theorem and, in 1930, to the notion of a Herbrand universe and a Herbrand interpretation that allowed (un)satisfiability of first-order formulas (and hence the validity of a theorem) to be reduced to (potentially infinitely many) propositional satisfiability problems.[5]

In 1929, Mojżesz Presburger showed that the theory of natural numbers with addition and equality (now called Presburger arithmetic in his honor) is decidable and gave an algorithm that could determine if a given sentence in the language was true or false.[6][7] However, shortly after this positive result, Kurt Gödel published On Formally Undecidable Propositions of Principia Mathematica and Related Systems (1931), showing that in any sufficiently strong axiomatic system there are true statements which cannot be proved in the system. This topic was further developed in the 1930s by Alonzo Church and Alan Turing, who on the one hand gave two independent but equivalent definitions of computability, and on the other gave concrete examples for undecidable questions.

First implementations

Shortly after World War II, the first general purpose computers became available. In 1954, Martin Davis programmed Presburger's algorithm for a JOHNNIAC vacuum tube computer at the Princeton Institute for Advanced Study. According to Davis, "Its great triumph was to prove that the sum of two even numbers is even".[7][8] More ambitious was the Logic Theory Machine, a deduction system for the propositional logic of the Principia Mathematica, developed by Allen Newell, Herbert A. Simon and J. C. Shaw. Also running on a JOHANNIAC, the Logic Theory Machine constructed proofs from a small set of propositional axioms and three deduction rules: modus ponens, (propositional) variable substitution, and the replacement of formulas by their definition. The system used heuristic guidance, and managed to prove 38 of the first 52 theorems of the Principia.[7]

The "heuristic" approach of the Logic Theory Machine tried to emulate human mathematicians, and could not guarantee that a proof could be found for every valid theorem even in principle. In contrast, other, more systematic algorithms achieved, at least theoretically, completeness for first-order logic. Initial approaches relied on the results of Herbrand and Skolem to convert a first-order formula into successively larger sets of propositional formulae by instantiating variables with terms from the Herbrand universe. The propositional formulas could then be checked for unsatisfiability using a number of methods. Gilmore's program used conversion to disjunctive normal form, a form in which the satisfiability of a formula is obvious.[7][9]

Decidability of the problem

Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but Co-NP-complete, and hence only exponential-time algorithms are believed to exist for general proof tasks. For a first order predicate calculus, with no ("proper") axioms, Gödel's completeness theorem states that the theorems (provable statements) are exactly the logically valid well-formed formulas, so identifying valid formulas is recursively enumerable: given unbounded resources, any valid formula can eventually be proven.

However, invalid formulas (those that are not entailed by a given theory), cannot always be recognized. In addition, a consistent formal theory that contains the first-order theory of the natural numbers (thus having certain "proper axioms"), by Gödel's incompleteness theorem, contains true statements which cannot be proven. In these cases, an automated theorem prover may fail to terminate while searching for a proof. Despite these theoretical limits, in practice, theorem provers can solve many hard problems, even in these undecidable logics.

Related problems

A simpler, but related, problem is proof verification, where an existing proof for a theorem is certified valid. For this, it is generally required that each individual proof step can be verified by a primitive recursive function or program, and hence the problem is always decidable.

Since the proofs generated by automated theorem provers are typically very large, the problem of proof compression is crucial and various techniques aiming at making the prover's output smaller, and consequently more easily understandable and checkable, have been developed.

Proof assistants require a human user to give hints to the system. Depending on the degree of automation, the prover can essentially be reduced to a proof checker, with the user providing the proof in a formal way, or significant proof tasks can be performed automatically. Interactive provers are used for a variety of tasks, but even fully automatic systems have proven a number of interesting and hard theorems, including at least one that has eluded human mathematicians for a long time, namely the Robbins conjecture.[10][11] However, these successes are sporadic, and work on hard problems usually requires a proficient user.

Another distinction is sometimes drawn between theorem proving and other techniques, where a process is considered to be theorem proving if it consists of a traditional proof, starting with axioms and producing new inference steps using rules of inference. Other techniques would include model checking, which, in the simplest case, involves brute-force enumeration of many possible states (although the actual implementation of model checkers requires much cleverness, and does not simply reduce to brute force).

There are hybrid theorem proving systems which use model checking as an inference rule. There are also programs which were written to prove a particular theorem, with a (usually informal) proof that if the program finishes with a certain result, then the theorem is true. A good example of this was the machine-aided proof of the four color theorem, which was very controversial as the first claimed mathematical proof which was essentially impossible to verify by humans due to the enormous size of the program's calculation (such proofs are called non-surveyable proofs). Another example would be the proof that the game Connect Four is a win for the first player.

Industrial uses

Commercial use of automated theorem proving is mostly concentrated in integrated circuit design and verification. Since the Pentium FDIV bug, the complicated floating point units of modern microprocessors have been designed with extra scrutiny. Nowadays, AMD, Intel and others use automated theorem proving to verify that division and other operations are correctly implemented in their processors.

First-order theorem proving

First-order theorem proving is one of the most mature subfields of automated theorem proving. The logic is expressive enough to allow the specification of arbitrary problems, often in a reasonably natural and intuitive way. On the other hand, it is still semi-decidable, and a number of sound and complete calculi have been developed, enabling fully automated systems. More expressive logics, such as higher order logics, allow the convenient expression of a wider range of problems than first order logic, but theorem proving for these logics is less well developed.

Benchmarks and competitions

The quality of implemented systems has benefited from the existence of a large library of standard benchmark examples — the Thousands of Problems for Theorem Provers (TPTP) Problem Library[12] — as well as from the CADE ATP System Competition (CASC), a yearly competition of first-order systems for many important classes of first-order problems.

Some important systems (all have won at least one CASC competition division) are listed below.

  • E is a high-performance prover for full first-order logic, but built on a purely equational calculus, developed primarily in the automated reasoning group of Technical University of Munich.
  • Otter, developed at the Argonne National Laboratory, is the first widely used high-performance theorem prover . It is based on first-order resolution and paramodulation. Otter has since been replaced by Prover9, which is paired with Mace4.
  • SETHEO is a high-performance system based on the goal-directed model elimination calculus. It is developed in the automated reasoning group of Technical University of Munich. E and SETHEO have been combined (with other systems) in the composite theorem prover E-SETHEO.
  • Alexandre Riazanov. It has won the CADE ATP System Competition in the most prestigious CNF (MIX) division for eleven years (1999, 2001–2010).
  • Waldmeister is a specialized system for unit-equational first-order logic. It has won the CASC UEQ division for the last fourteen years (1997–2010).
  • SPASS is a first order logic theorem prover with equality. This is developed by the research group Automation of Logic, Max Planck Institute for Computer Science.

Popular techniques

Comparison

See also: Proof assistant#Comparison and Category:Theorem proving software systems

Name License type Web service Library Standalone Version Last update (YYYY-mm-dd format) Author Notice
ACL2 3-clause BSD No No Yes 6.2 2013/06 Matt Kaufmann, J. Strother Moore -
Prover9 / Mace4 GPLv2 No Yes Yes v05 2009/11/04 William McCune / Argonne National Laboratory -
Otter Public Domain Via System on TPTP Yes No 3.3f 2004/09 William McCune / Argonne National Laboratory Succeeded by Prover9 / Mace4
j'Imp ? No No Yes - 2010/05/28 André Platzer -
Metis ? No Yes No 2.2 2010/05/24 Joe Hurd -
Jape ? Yes Yes No 1.0 2010/03/22 Adolfo Gustavo Neto, USP -
PVS ? No Yes No 4.2 2008/07 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 2009/05 William McCune / Argonne National Laboratory -
SAD ? Yes Yes No 2.3-2.5 2008/08/27 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 2012/05 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 2011/08/20 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 1996/10 Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela Pilar Nivela -
Theorem Proving System (TPS) ? No Yes No - 2004/06/24 Carnegie Mellon University -
SPASS ? Yes Yes Yes 3.7 2005/11 Max Planck Institut Informatik -
IsaPlanner GPL No Yes Yes IsaPlanner 2 2007 Lucas Dixon, Johansson Moa -
KeY GPL Yes Yes Yes 1.6 2010/10 Karlsruhe Institute of Technology, Chalmers University of Technology, University of Koblenz -
Theorem Checker ? No No Yes 0 2013 Robert J. Swartz, Northeastern Illinois University -
Princess GPL Via Java Webstart and System on TPTP Yes Yes 2012-11-02 2012 Philipp Rümmer, Uppsala University -

Free software

Proprietary software

  • Acumen RuleManager (commercial product)
  • ALLIGATOR
  • CARINE
  • KIV
  • Prover Plug-In (commercial proof engine product)
  • ProverBox
  • ResearchCyc
  • Spear modular arithmetic theorem prover

Notable people

  • Leo Bachmair, co-developer of the superposition calculus.
  • Woody Bledsoe, artificial intelligence pioneer.
  • Robert S. Boyer, co-author of the Boyer-Moore theorem prover, co-recipient of the Herbrand Award 1999.
  • Alan Bundy, University of Edinburgh, meta-level reasoning for guiding inductive proof, proof planning and recipient of 2007 IJCAI Award for Research Excellence, Herbrand Award, and 2003 Donald E. Walker Distinguished Service Award.
  • William McCune Argonne National Laboratory, author of Otter, the first high-performance theorem prover. Many important papers, recipient of the Herbrand Award 2000.
  • ENS Cachan. Many important papers.
  • Robert Lee Constable, Cornell University. Important contributions to type theory, NuPRL.
  • Martin Davis, author of the "Handbook of Artificial Reasoning", co-inventor of the DPLL algorithm, recipient of the Herbrand Award 2005.
  • Branden Fitelson University of California at Berkeley. Work in automated discovery of shortest axiomatic bases for logic systems.
  • Harald Ganzinger, co-developer of the superposition calculus, head of the MPI Saarbrücken, recipient of the Herbrand Award 2004 (posthumous).
  • Stanford University professor of Computer Science.
  • Keith Goolsbey chief developer of the Cyc inference engine.
  • Michael J. C. Gordon led the development of the HOL theorem prover.
  • Gérard Huet Term rewriting, HOL logics, Herbrand Award 1998.
  • Robert Kowalski developed the connection graph theorem-prover and SLD resolution, the inference engine that executes logic programs.
  • model elimination, recipient of the Herbrand Award 2001.
  • Norman Megill, developer of metamath.org, an online database of automatically verified proofs.
  • J Strother Moore, co-author of the Boyer-Moore theorem prover, co-recipient of the Herbrand Award 1999.
  • Robert Nieuwenhuis University of Barcelona. Co-developer of the superposition calculus.
  • Tobias Nipkow of the Technical University of Munich, contributions to (higher-order) rewriting, co-developer of the Isabelle proof assistant
  • The Fellowship for Interpretation of Genomes
  • Lawrence C. Paulson of the University of Cambridge, work on higher-order logic system, co-developer of the Isabelle Theorem Prover
  • David Plaisted University of North Carolina at Chapel Hill. Complexity results, contributions to rewriting and completion, instance-based theorem proving.
  • John Rushby Program Director - SRI International[13]
  • J. Alan Robinson Syracuse University. Developed original resolution and unification based first order theorem proving, co-editor of the "Handbook of Automated Reasoning", recipient of the Herbrand Award 1996
  • Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements
  • Stephan Schulz, E theorem Prover.
  • Natarajan Shankar SRI International, work on decision procedures, little engines of proof, co-developer of PVS.
  • Mark Stickel SRI International. Recipient of the Herbrand Award 2002.
  • Geoff Sutcliffe University of Miami. Maintainer of the TPTP collection, an organizer of the CADE annual contest.
  • Dolph Ulrich Purdue, Work on automated discovery of shortest axiomatic bases for systems.
  • Robert Veroff University of New Mexico. Many important papers.
  • Andrei Voronkov Developer of Vampire and Co-Editor of the "Handbook of Automated Reasoning"
  • Larry Wos Argonne National Laboratory. (Otter) Many important papers. Very first Herbrand Award winner (1992)
  • Wen-Tsun Wu Work in geometric theorem proving: Wu's method, Herbrand Award 1997
  • Christoph Weidenbach, author of SPASS, automated theorem prover.

See also

Notes

References

This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
 
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
 
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.
 


Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.