**Automated theorem proving** (**ATP**) or *automated deduction*, currently the most well-developed subfield of *automated reasoning* (AR), is the proving of mathematical theorems by a computer program. Automated reasoning is an area of Computer Science dedicated to creating software which allows to perform reasoning on computers completely or nearly completely automatically. ...
In mathematics, a proof is a demonstration that, assuming certain axioms, some statement is necessarily true. ...
Look up theorem in Wiktionary, the free dictionary. ...
## Decidability of the problem
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 general proof tasks. For a first order predicate calculus, that is having no **proper axioms**, **Gödel's Completeness Theorem** states that the theorems are exactly the logically valid well-formed formulas, so identifying theorems 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 addition, a consistent **formal theory** that contains the **first-order theory of the natural numbers** (having certain **proper axioms** then), by Gödel's incompleteness theorems, contains a true statement which cannot be proven, in which case a theorem prover trying to prove such a statement ends up in nontermination. Propositional logic or sentential logic is the logic of propositions, sentences, or clauses. ...
In complexity theory, the NP-complete problems are the most difficult problems in NP, in the sense that they are the ones most likely not to be in P. The reason is that if you could find a way to solve an NP-complete problem quickly, then you could use...
First-order logic (FOL) is a universal language in symbolic science, and is in use everyday by mathematicians, philosophers, linguists, computer scientists and practitioners of artificial intelligence. ...
In logic, WFF is an abbreviation for well-formed formula. ...
In computability theory, often less suggestively called recursion theory, a countable set S is called recursively enumerable, computably enumerable, semi-decidable or provable if There is an algorithm that, when given an input — typically an integer or a tuple of integers or a sequence of characters — eventually halts...
In mathematical logic, GÃ¶dels incompleteness theorems, proved by Kurt GÃ¶del in 1931, are two theorems stating inherent limitations of all but the most trivial formal systems for arithmetic of mathematical interest. ...
In these cases, a first-order theorem prover may fail to terminate while searching for a proof. Despite these theoretical limits, practical theorem provers can solve many hard problems in these 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. Proof checking is the process of using software for checking proofs for correctness. ...
In computability theory, primitive recursive functions are a class of functions which form an important building block on the way to a full formalization of computability. ...
*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. Interactive theorem proving is the field of computer science and mathematical logic concerned with tools to develop formal proofs by man-machine collaboration. ...
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. Model checking is a method to algorithmically verify formal systems. ...
Example of a four-colored map The four color theorem (also known as the four color map theorem) states that given any plane separated into regions, such as a political map of the counties of a state, the regions may be colored using no more than four colors in such...
Connect Four (also known as Plot Four) is a two-player board game in which the objective is to be the first to get four of ones own discs in a line. ...
## 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. In the latest processors from AMD, Intel, and others, automated theorem proving has been used to verify that division and other operations are correct. On October 30, 1994, Professor Thomas Nicely who was then at Lynchburg College reported a bug in the Pentium floating point unit. ...
A floating point unit (FPU) is a part of a computer system specially designed to carry out operations on floating point numbers. ...
Advanced Micro Devices, Inc. ...
Intel Corporation (NASDAQ: INTC, SEHK: 4335), founded in 1968 as Integrated Electronics Corporation, is an American multinational corporation that is best known for designing and manufacturing microprocessors and specialized integrated circuits. ...
## First-order theorem proving So called **first-order theorem proving** may be restricted to a propositional calculus with **terms** (constants, function names, and free variables) added, making it impossible to express mathematical induction. It should then not be confused with a first-order theory of metamathematics, as the quantifiers have been stripped out, though universal quantifiers may be emulated by rewriting into free variables. In logic and mathematics, a propositional calculus (or a sentential calculus) is a formal system in which formulas representing propositions can be formed by combining atomic propositions using logical connectives, and a system of formal proof rules allows to establish that certain formulas are theorems of the formal system. ...
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers. ...
First-order logic (FOL) is a universal language in symbolic science, and is in use everyday by mathematicians, philosophers, linguists, computer scientists and practitioners of artificial intelligence. ...
In general, metamathematics or meta-mathematics is reflection about mathematics seen as an entity/object in human consciousness and culture. ...
In language and logic, quantification is a construct that specifies the extent of validity of a predicate, that is the extent to which a predicate holds over a range of things. ...
In predicate logic, universal quantification is an attempt to formalise the notion that something (a logical predicate) is true for everything, or every relevant thing. ...
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 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. First-order logic (FOL) is a universal language in symbolic science, and is in use everyday by mathematicians, philosophers, linguists, computer scientists and practitioners of artificial intelligence. ...
CADE is the the premier scientific conference on automated deduction and related fields. ...
Some important systems (all have won at least one CASC competition division) are listed below. E is a modern, high performance theorem prover for first-order logic with equality. ...
This is due to the donkey field created by horses consuming large amounts of alcohol, if this is trtue then xt must be equal to Wc and thus sheep are white. ...
Munich University of Technology, or Technical University of Munich (TUM) (in German: Technische UniversitÃ¤t MÃ¼nchen, TUM), is a major German university located in Munich (and the towns of Garching and Freising outside of Munich). ...
Otter is an automated theorem prover developed at the Argonne National Laboratory in Illinois. ...
Aerial photo of the Advanced Photon Source at Argonne National Laboratory. ...
In mathematical logic and automated theorem proving, a branch of the traditional artificial intelligence (see GOFAI), resolution is a theorem-proving technique for sentences in propositional logic and first-order logic. ...
Model Elimination is the name attached to a pair of proof procedures invented by Donald W. Loveland, the first of which was published in 1968 in the Journal of the ACM. Their primary purpose is to carry out Automated theorem proving, though they can readily be extended to Logic programming...
Munich University of Technology, or Technical University of Munich (TUM) (in German: Technische UniversitÃ¤t MÃ¼nchen, TUM), is a major German university located in Munich (and the towns of Garching and Freising outside of Munich). ...
Vampire is an automatic theorem prover for first-order classical logic developed in the Computer Science Department of the University of Manchester. ...
## Popular techniques In mathematical logic and automated theorem proving, a branch of the traditional artificial intelligence (see GOFAI), resolution is a theorem-proving technique for sentences in propositional logic and first-order logic. ...
In mathematical logic, in particular as applied to computer science, a unification of two terms is a join (in the lattice sense) with respect to a specialisation order. ...
A lean theorem prover is an automated theorem prover implemented in a minimum amount of code. ...
Model Elimination is the name attached to a pair of proof procedures invented by Donald W. Loveland, the first of which was published in 1968 in the Journal of the ACM. Their primary purpose is to carry out Automated theorem proving, though they can readily be extended to Logic programming...
Analytic tableaux, or, more briefly, just tableaux, are a fundamental concept in automated theorem proving. ...
This is due to the donkey field created by horses consuming large amounts of alcohol, if this is trtue then xt must be equal to Wc and thus sheep are white. ...
Rewriting in mathematics, computer science and logic covers a wide range of methods of transforming strings, written in some fixed alphabet, that are not deterministic but are governed by explicit rules. ...
Model checking is a method to algorithmically verify formal systems. ...
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers. ...
A binary decision diagram (BDD), like a negation normal form (NNF) or a propositional directed acyclic graph (PDAG), is a data structure that is used to represent a Boolean function. ...
The DPLL/Davis-Putnam-Logemann-Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i. ...
## Available implementations 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. ACL2 is a software system consisting of a programming language, an extensible theory in a first-order logic, and a mechanical theorem prover. ...
Automath (automating mathematics) is a programming language, devised by Nicolaas Govert de Bruijn, for expressing complete mathematical theories in such a way that a Theorem prover can verify the correctness. ...
CARINE is a first-order classical logic automated theorem prover. ...
Coq is a proof assistant which handles mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. ...
CVC (for Cooperating Validity Checker) is an automatic theorem prover for the Satisfiability Modulo Theories problem. ...
E is a modern, high performance theorem prover for first-order logic with equality. ...
The Isabelle theorem prover is an interactive theorem proving framework, a successor of the HOL theorem prover. ...
The Gandalf theorem prover is the first-order theorem prover applied to several domain-specific tasks such as Semantic web. ...
The various HOL (which stands for Higher Order Logic) systems are a family of interactive theorem proving systems sharing similar logics and implementation strategies. ...
HOL Light is a member of the HOL theorem prover family. ...
An interactive theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others. ...
Matita is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna. ...
The Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referred to and used in new articles. ...
This article lacks information on the importance of the subject matter. ...
Otter is an automated theorem prover developed at the Argonne National Laboratory in Illinois. ...
Paradox is an automated theorem proving system. ...
In automated theorem proving, PhoX is a Proof assistant based on Higher Order logic which is eXtensible. ...
PVS, or the Prototype Verification System, is a specification language integrated with support tools and a theorem prover, developed at the Computer Science Laboratory of SRI International. ...
Cyc is an artificial intelligence project which attempts to assemble a comprehensive ontology and database of everyday common-sense knowledge, with the goal of enabling AI applications to perform human-like reasoning. ...
SPARK is a secure, formally-defined language designed to support the development of software used in applications where correct operation is vital either for reasons of safety or business integrity. ...
Tau is a robust and general purpose, interactive (live on the web), user-configurable automated theorem prover for first-order predicate logic with equality. ...
The Theorem Proving System (TPS) is an automated theorem proving system for first-order and higher-order logic. ...
Twelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory. ...
Vampire is an automatic theorem prover for first-order classical logic developed in the Computer Science Department of the University of Manchester. ...
## Important 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 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.
- 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, 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.
- Robert Kowalski developed the connection graph theorem-prover and SLD resolution, the inference engine that executes logic programs.
- Donald W. Loveland Duke University. Author, co-developer of the DPLL-procedure, developer of model elimination, recipient of the Herbrand Award 2001.
- Sergei Maslov
- Norman Megill, maintainer 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 Technical University of Munich, contributions to (higher-order) rewriting, co-developer of the Isabelle, proof assistant
- Ross Overbeek Argonne National Laboratory. Founder of 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 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 Developer of Vampire and Co-Editor of the "Handbook of Automated Reasoning"
- Larry Wos Argonne National Laboratory. (Otter) Many important papers.
This is due to the donkey field created by horses consuming large amounts of alcohol, if this is trtue then xt must be equal to Wc and thus sheep are white. ...
Woody Bledsoe Woodrow Wilson Woody Bledsoe (born November 12, 1921 Maysville, Oklahoma. ...
Garry Kasparov playing against Deep Blue, the first machine to win a chess game against a reigning world champion. ...
Robert Stephen Boyer, also known as Bob Boyer, is a professor of computer science, mathematics, and philosophy at The University of Texas at Austin. ...
The Herbrand Award for exceptional contributions to the field of Automated Deduction is an award given by CADE Inc. ...
Year 1999 (MCMXCIX) was a common year starting on Friday (link will display full 1999 Gregorian calendar). ...
Alan Bundy is a professor at the School of Informatics at the University of Edinburgh, known for his contributions to automated reasoning, especially to proof-planning (the use of meta-level reasoning to guide proof search [1]). He is the leader of the DReaM group (Mathematical Reasoning Group), the world...
The University of Edinburgh, founded in 1582,[4] is a renowned centre for teaching and research in Edinburgh, Scotland. ...
Sir Robert Constable (ca. ...
The DPLL/Davis-Putnam-Logemann-Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i. ...
Harald Ganzinger (October 31, 1950 - June 3, 2004) was a German computer scientist that together with Leo Bachmair developed the superposition calculus, which is (as of 2007) used in most of the state-of-the-art automated theorem provers for first-order logic. ...
The Herbrand Award for exceptional contributions to the field of Automated Deduction is an award given by CADE Inc. ...
shelby was here 2004 (MMIV) was a leap year starting on Thursday of the Gregorian calendar. ...
Leland Stanford Junior University, commonly known as Stanford University (or simply Stanford), is a private university located approximately 37 miles (60 kilometers) southeast of San Francisco and approximately 20 miles northwest of San JosÃ© in Stanford, California. ...
Cyc is an artificial intelligence project that attempts to assemble a comprehensive ontology and database of everyday common sense knowledge, with the goal of enabling AI applications to perform human-like reasoning. ...
Michael J.C. Gordon, British computer scientist (born 28 February 1948). ...
Robert Anthony Kowalski (Bob Kowalski, born May 15, 1941 in Bridgeport, Connecticut, USA) is an American logician and computer scientist, who has spent much of his career in the UK. He was educated at the University of Chicago, University of Bridgeport (BA in mathematics, 1963), Stanford University (MSc in mathematics...
Logic programming (which might better be called logical programming by analogy with mathematical programming and linear programming) is, in its broadest sense, the use of mathematical logic for computer programming. ...
Model Elimination is the name attached to a pair of proof procedures invented by Donald W. Loveland, the first of which was published in 1968 in the Journal of the ACM. Their primary purpose is to carry out Automated theorem proving, though they can readily be extended to Logic programming...
The Herbrand Award for exceptional contributions to the field of Automated Deduction is an award given by CADE Inc. ...
Year 2001 (MMI) was a common year starting on Monday of the Gregorian calendar. ...
J Strother Moore is a computer scientist, and is co-developer of the Boyer-Moore string search algorithm and the Boyer-Moore automated theorem prover, NQTHM. A good example of the workings of the Boyer-Moore string search algorithm is given in his website along with the Knuth-Morris-Pratt...
Munich University of Technology, or Technical University of Munich (TUM) (in German: Technische UniversitÃ¤t MÃ¼nchen, TUM), is a major German university located in Munich (and the towns of Garching and Freising outside of Munich). ...
The Isabelle theorem prover is an interactive theorem proving framework, a successor of the HOL theorem prover. ...
Ross Overbeek is an American Computer Scientist. ...
Lawrence Paulson (born 1955) is a professor at the University of Cambridge Computer Laboratory and a fellow of Clare College. ...
The University of Cambridge (often Cambridge University), located in Cambridge, England, is the second-oldest university in the English-speaking world and has a reputation as one of the worlds most prestigious universities. ...
The University of North Carolina at Chapel Hill is a public, coeducational, research university located in Chapel Hill, North Carolina, United States. ...
Rewriting in mathematics, computer science and logic covers a wide range of non-deterministic methods of replacing subterms of a formula with other terms. ...
The Knuth-Bendix completion algorithm is an algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. ...
SRI Internationals main campus on Ravenswood Avenue, Menlo Park, California SRI International is one of the worlds largest contract research institutions. ...
SRI Internationals main campus on Ravenswood Avenue, Menlo Park, California SRI International is one of the worlds largest contract research institutions. ...
PVS, or the Prototype Verification System, is a specification language integrated with support tools and a theorem prover, developed at the Computer Science Laboratory of SRI International. ...
An acronym SRI may refer to one of the following: Socially Responsible Investment. ...
## References - Chin-Liang Chang; Richard Char-Tung Lee (1973).
*Symbolic Logic and Mechanical Theorem Proving*. Academic Press. - Loveland, Donald W. (1978).
*Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6*. North-Holland Publishing. - Gallier, Jean H. (1986).
*Logic for Computer Science: Foundations of Automatic Theorem Proving*. Harper & Row Publishers. - Duffy, David A. (1991).
*Principles of Automated Theorem Proving*. John Wiley & Sons. - Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992).
*Automated Reasoning: Introduction and Applications*, 2nd edition, McGraw-Hill. - (2001) in Alan Robinson and Andrei Voronkov (eds.):
*Handbook of Automated Reasoning Volume I & II*. Elsevier and MIT Press. - Fitting, Melvin (1996).
*First Order and Automated Theorem Proving*, 2nd edition, Springer. Academic Press (London, New York and San Diego) was an academic book publisher that is now part of Elsevier. ...
The Wiley Building in Hoboken, New Jersey, located on the waterfront between River Street and Frank Sinatra Drive. ...
The McGraw-Hill Companies logo. ...
Elseviers logo. ...
MIT Press Books The MIT Press is a university publisher affiliated with the Massachusetts Institute of Technology (MIT) in Cambridge, Massachusetts. ...
Springer Science+Business Media or Springer (IPA: ) is a worldwide publishing company based in Germany which focuses on academic journals and books in the fields of science, technology, mathematics, and medicine. ...
## See also |