Automated theorem proving
From Exampleproblems
Automated theorem proving (currently the most important subfield of automated reasoning) is the proving of mathematical theorems by a computer program. Depending on the underlying logic, the problem of deciding the validity of a theorem varies from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but NP-complete, and hence only exponential time algorithms are believed to exist. For first-order logic it is recursively enumerable, i.e., given unbounded resources, any valid theorem can eventually be proven. Invalid statements, i.e. formulas that are not entailed by a given theory, cannot always be recognized. In these cases, a first-order theorem prover will fail to terminate while searching for a proof. Despite these theoretical limits, practical theorem provers can solve many hard problems in these logics.
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.
Interactive theorem provers 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 by now proven a number of interesting and hard theorems, including some that have eluded human mathematicians for a long time. 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 is equivalent to 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.
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. In the latest processors from AMD, Intel, and others, automated theorem proving has been used to verify that the divide and other operations are correct.
Contents |
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. The quality of implemented system has benefited by the existence of a large library of standard benchmark examples (the TPTP), as well as by the CADE ATP System Competition (CASC), a yearly competition of first-order systems for many important classes of first-order problems.
Some important system (all have won at least one CASC competition division) are listed below.
- E is a high-performance prover 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.
- 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.
- Vampire is developed and implemented at Manchester University by Andrei Voronkov, formerly together with Alexandre Riazanov. It has won the "world cup for theorem provers" (the CADE ATP (Automated theorem prover) System Competition) in the most prestigious MIX division for six years (1999, 2001 - 2005).
- Waldmeister is a specialized system for unit-equational first-order logic. It has won the CASC UEQ division for the last nine years (1997-2005).
Popular techniques
- First-order resolution with Unification
- Method of analytic tableaux
- Superposition and term rewriting
- Model checking
- Mathematical induction
- Binary decision diagrams
- DPLL
- Higher-order unification
Available implementations
- ACL2
- Carine
- Coq
- CVC Lite
- E
- Isabelle
- Gandalf
- HOL
- LCF
- MetaPRL
- Mizar
- NuPRL
- Otter
- Paradox
- PhoX
- PVS
- Simplify
- SPASS
- Twelf
- Vampire
- Waldmeister
You can find information on some of these theorem provers and others at http://www.tptp.org/CASC/J2/SystemDescriptions.html, or the QPQ website. The TPTP library of test problems, suitable for testing first-order theorem provers, is available at http://www.tptp.org, and solutions from many of these provers for TPTP problems are in the TSTP solution library, available at http://www.tptp.org/TSTP .
Important people
- Leo Bachmair Co-developer of the superposition calculus.
- Robert Stephen Boyer Co-Author of the Boyer-Moore theorem prover, co-recipient of the Herbrand Award 1999.
- William McCune Argonne National Laboratory. Author of Otter, the first high-performance theorem prover. Many important papers, recipient of the Herbrand Award 2000.
- Robert 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 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).
- Michael Genesereth
- Michael J. C. Gordon Led the development of the HOL theorem prover.
- Donald W. Loveland Duke University. Author, co-developer of the DPLL-procedure, developer of Model Elimination, recipient of the Herbrand Award 2001.
- Sergei Maslov
- 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 Technical University of Munich, contributions to (higher-order) rewriting, co-developer of the Isabelle proof assistant
- Ross Overbeek
- Lawrence C. Paulson University of Cambridge, work on higher-order logic system, co-developer of the Isabelle proof assistant
- David A. 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
- 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
- Natarajan Shankar SRI International, work on decision procedures, little engines of proof, co-developer of PVS.
- Mark Stickel SRI. Recipient of the Herbrand Award 2002.
- Geoff Sutcliffe University of Miami. Maintainer of the TPTP collection, an organizer of the CADE annual contest.
- Robert Veroff University of New Mexico. Many important papers.
- Andrei Voronkov Co-Editor of the "Handbook of Automated Reasoning"
- Larry Wos Argonne National Laboratory. (Otter) Many important papers.
References (books)
- Symbolic Logic and Mechanical Theorem Proving. Chin-Liang Chang and Richard Char-Tung Lee. Academic Press (1973)
- Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6. Donald W. Loveland. North-Holland Publishing (1978)
- Logic for Computer Science: Foundations of Automatic Theorem Proving. Jean H. Gallier. Harper & Row Publishers (1986) Download
- Principles of Automated Theorem Proving. David A. Duffy. John Wiley & Sons (1991)
- Automated Reasoning: Introduction and Applications (2nd edition). Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. McGraw-Hill (1992)
- Handbook of Automated Reasoning Volume I & II. Alan Robinson and Andrei Voronkov (eds.) Elsevier and MIT Press (2001)