- Automated theorem proving
**Automated theorem proving**(**ATP**) or**automated deduction**, currently the most well-developed subfield of "automated reasoning " (AR), is the proving ofmathematical theorem s by acomputer program .**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 butNP-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 isrecursively 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"), byGödel's incompleteness theorem , contains a true statement 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 aprimitive 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 proven a number of interesting and hard theorems, including some that have eluded human mathematicians for a long time. [

*cite journal|author=W.W. McCune|title=Solution of the Robbins Problem|journal=Journal of Automated Reasoning|year=1997|url=http://www.springerlink.com/content/h77246751668616h/|volume=19|issue=3*] [*cite news|title=Computer Math Proof Shows Reasoning Power|author=Gina Kolata|date=December 10, 1996|url=http://www.nytimes.com/library/cyber/week/1210math.html|publisher=*] However, these successes are sporadic, and work on hard problems usually requires a proficient user.The New York Times |accesdate=2008-10-11Another 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 callednon-surveyable proofs ). Another example would be the proof that the gameConnect 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 complicatedfloating point unit s of modern microprocessors have been designed with extra scrutiny. In the latest processors fromAMD ,Intel , and others, automated theorem proving has been used to verify that division and other operations are correct.**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 and modal 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. The quality of implemented system has benefited from the existence of a large library of standard benchmark examples - the Thousands of Problems for Theorem Provers (TPTP) Problem Library [

*http://www.cs.miami.edu/~tptp/*] - as well as from the CADE ATP System Competition ( [*http://www.cs.miami.edu/~tptp/CASC 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 theArgonne National Laboratory , is the first widely used high-performance theorem prover. It is based onfirst-order resolution andparamodulation . Otter has since been replaced by Prover9, which is paired withMace4 .

*SETHEO is a high-performance system based on the goal-directedmodel elimination calculus. It is developed in the automated reasoning group ofTechnical 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 [*http://www.manchester.ac.uk/ Manchester University*] by [*http://www.cs.man.ac.uk/~voronkov/ Andrei Voronkov*] , formerly together with [*http://www.freewebs.com/riazanov/ Alexandre Riazanov*] . It has won the "world cup for theorem provers" ( [*http://www.cs.miami.edu/~tptp/CASC/ the CADE ATP System Competition*] ) in the most prestigious CNF (MIX) division for eight years (1999, 2001 - 2007).

*Waldmeister is a specialized system for unit-equational first-order logic. It has won the CASC UEQ division for the last ten years (1997-2006).**Popular techniques***

First-order resolution withunification

*Lean theorem proving

*Model elimination

*Method of analytic tableaux

*Superposition and termrewriting

*Model checking

*Mathematical induction

*Binary decision diagram s

*DPLL

*Higher-order unification **Available implementations**"See also:"

**Free software**

*ACL2

* Automath

*Coq

* CVC

* E

*EQP

* Gandalf

* [*http://www.idsia.ch/~juergen/goedelmachine.html Gödel-machines*]

* HOL

*HOL Light

* Isabelle

*Jape

*KeY

* LCF

* [*http://www.ags.uni-sb.de/~leo Leo II*]

* [*http://www.irit.fr/ACTIVITES/LILaC/Lotrec/ LoTREC*]

* [*http://metaprl.org/ MetaPRL*]

*Matita

*NuPRL

* Otter

* Paradox

*PhoX

* [*http://www.lemma-one.com/ProofPower/index/index.html ProofPower*]

*Prover9 /Mace4

* PVS

* SNARK

* Tau**Proprietary software including Share-alike Non-commercial**

* [*http://www.acumenbusiness.com/Components/ComponentsDetail.htm#verification-validation Acumen RuleManager*] (commercial product)

* [*http://mcs.open.ac.uk/pp2464/alligator/ Alligator*]

*CARINE

* [*http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/kiv/ KIV*]

* Mizar

* [*http://www.prover.com/products/prover_plugin/ Prover Plug-In*] (commercial proof engine product)

* [*http://www.ub-net.de/cms/proverbox.html ProverBox*]

*ResearchCyc

* Simplify

*SPARK (programming language)

* [*http://spass.mpi-sb.mpg.de/ SPASS*]

* [*http://www.cs.ubc.ca/~babic/index_spear.htm Spear modular arithmetic theorem prover*]

*Theorem Proving System (TPS)

*Twelf

* Vampire/Vampyre

* [*http://www.waldmeister.org/ Waldmeister*]You can find information on some of these theorem provers and others at http://www.tptp.org/CASC/J2/SystemDescriptions.html . 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.

**Notes****Important people***

Leo Bachmair , co-developer of thesuperposition calculus .

*Woody Bledsoe ,artificial intelligence pioneer.

*Robert S. Boyer , co-author of the Boyer-Moore theorem prover, co-recipient of theHerbrand Award 1999.

*Alan Bundy ,University of Edinburgh , meta-level reasoning for guiding inductive proof, proof planning and recipient of 2007IJCAI Award for Research Excellence andHerbrand Award , and 2003 Donald E. Walker Distinguished Service Award.

* [*http://www-unix.mcs.anl.gov/~mccune/ William McCune*] Argonne National Laboratory, author of Otter, the first high-performance theorem prover. Many important papers, recipient of theHerbrand Award 2000.

* [*http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon*] ,CNRS and nowENS Cachan . Many important papers.

*Robert Constable , Cornell University. Important contributions to type theory, NuPRL.

* [*http://www.cs.nyu.edu/cs/faculty/davism/ Martin Davis*] , author of the "Handbook of Artificial Reasoning", co-inventor of theDPLL algorithm , recipient of theHerbrand Award 2005.

* [*http://www.fitelson.org/ 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 theHerbrand Award 2004 (posthumous).

* [*http://logic.stanford.edu/people/genesereth/ Michael Genesereth*] ,Stanford University professor of Computer Science.

*Keith Goolsbey chief developer of theCyc inference engine.

*Michael J. C. Gordon led the development of the HOL theorem prover.

* [*http://pauillac.inria.fr/~huet/ Gerard Huet*] Term rewriting, HOL logics,Herbrand Award 1998

*Robert Kowalski developed the connection graph theorem-prover andSLD resolution , the inference engine that executes logic programs.

* [*http://www.cs.duke.edu/~dwl/ Donald W. Loveland*] Duke University. Author, co-developer of the DPLL-procedure, developer ofmodel elimination , recipient of theHerbrand Award 2001.

* Norman Megill, developer ofMetamath , and maintainer of its site at [*http://www.metamath.org 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 Technical University of Munich , contributions to (higher-order) rewriting, co-developer of the Isabelle, proof assistant

*Ross Overbeek Argonne National Laboratory. Founder of [*http://theseed.uchicago.edu/FIG/Html/FIG.html The Fellowship for Interpretation of Genomes*]

*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 torewriting and completion, instance-based theorem proving.

* [*http://www.csl.sri.com/users/rushby/ 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 theHerbrand Award 1996

*Jürgen Schmidhuber Work on [*http://www.idsia.ch/~juergen/goedelmachine.html Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements*]

* [*http://www4.informatik.tu-muenchen.de/~schulz/ Stephan Schulz*] , E theorem Prover.

*Natarajan Shankar SRI International , work on decision procedures, "little engines of proof", co-developer of PVS.

*Mark Stickel SRI . Recipient of theHerbrand Award 2002.

* [*http://www.cs.miami.edu/~geoff/ Geoff Sutcliffe*] University of Miami. Maintainer of the TPTP collection, an organizer of the CADE annual contest.

* [*http://web.ics.purdue.edu/~dulrich/Home-page.htm Dolph Ulrich*] Purdue, Work on automated discovery of shortest axiomatic bases for systems.

* [*http://www.cs.unm.edu/~veroff/ Robert Veroff*] University of New Mexico. Many important papers.

* [*http://www.voronkov.com/ Andrei Voronkov*] Developer of Vampire and Co-Editor of the "Handbook of Automated Reasoning"

* [*http://www-unix.mcs.anl.gov/~wos/ Larry Wos*] Argonne National Laboratory. (Otter) Many important papers. Very firstHerbrand Award winner (1992)

* [*http://www.mmrc.iss.ac.cn/~wtwu/ Wen-Tsun Wu*] Work in geometric theorem proving,Herbrand Award 1997**References*** cite book | title = Symbolic Logic and Mechanical Theorem Proving

author = Chin-Liang Chang

coauthors = Richard Char-Tung Lee

publisher =Academic Press 1

year = 1973

* cite book

last = Loveland

first = Donald W.

title = Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6

publisher =North-Holland Publishing

year = 1978

* cite book

last = Gallier

first = Jean H.

title = Logic for Computer Science: Foundations of Automatic Theorem Proving

publisher =Harper & Row Publishers

year = 1986

url = http://www.cis.upenn.edu/~jean/gbooks/logic.html

* cite book

last = Duffy

first = David A.

title = Principles of Automated Theorem Proving

year = 1991

publisher =John Wiley & Sons

* cite book

last = Wos

first = Larry

coauthors = Overbeek, Ross; Lusk, Ewing; Boyle, Jim

title = Automated Reasoning: Introduction and Applications

edition = 2nd edition

publisher =McGraw-Hill

year = 1992

* cite book

title = Handbook of Automated Reasoning Volume I & II

editor = Alan Robinson and Andrei Voronkov (eds.)

publisher =Elsevier andMIT Press

year = 2001

* cite book

last = Fitting

first = Melvin

title = First-Order Logic and Automated Theorem Proving

edition = 2nd edition

publisher = Springer

year = 1996

url = http://comet.lehman.cuny.edu/fitting/**Notes****See also**

*Symbolic computation

*Computer-aided proof

*Automated reasoning

*Formal verification

*Logic programming

*Proof checking

*Model checking

*Proof complexity

*Computer algebra system

*Wikimedia Foundation.
2010.*