Automated theorem proving

automated theorem provertheorem provertheorem provingautomated deductiontheorem proversautomated theorem proversautomatic theorem provingautomatic theorem provermechanical theorem provingautomated theorem proving systems
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.wikipedia
282 Related Articles

Automated reasoning

reasoningautomated reasoning programautomatic reasoning
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.
The most developed subareas of automated reasoning are automated theorem proving (and the less automated but more pragmatic subfield of interactive theorem proving) and automated proof checking (viewed as guaranteed correct reasoning under fixed assumptions).

First-order logic

predicate logicfirst-orderpredicate calculus
Frege's Begriffsschrift (1879) introduced both a complete propositional calculus and what is essentially modern predicate logic. For a first order predicate calculus, 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.
Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in first-order logic.

Disjunctive normal form

disjunctiveDNF2-DNF
Gilmore's program used conversion to disjunctive normal form, a form in which the satisfiability of a formula is obvious.
As a normal form, it is useful in automated theorem proving.

Proof compression

proof reduction
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.
The developed algorithms can be used to improve the proofs generated by automated theorem proving tools such as sat-solvers, SMT-solvers, first-order theorem provers and proof assistants.

E (theorem prover)

E
E is a high-performance prover for full first-order logic, but built on a purely equational calculus, originally developed in the automated reasoning group of Technical University of Munich, and now at Baden-Württemberg Cooperative State University in Stuttgart.
E is a high performance theorem prover for full first-order logic with equality.

Presburger arithmetic

PresburgerPresburger’s decision procedure
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.
Because Presburger arithmetic is decidable, automatic theorem provers for Presburger arithmetic exist.

Mathematical logic

formal logicsymbolic logiclogic
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.
Computer science also contributes to mathematics by developing techniques for the automatic checking or even finding of proofs, such as automated theorem proving and logic programming.

CADE ATP System Competition

CASC
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 — 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.
The CADE ATP System Competition (CASC) is a yearly competition of fully automated theorem provers for classical logic CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organized by the Association for Automated Reasoning.

Superposition calculus

superpositionpurely equational calculus
E is a high-performance prover for full first-order logic, but built on a purely equational calculus, originally developed in the automated reasoning group of Technical University of Munich, and now at Baden-Württemberg Cooperative State University in Stuttgart. Superposition and term rewriting
The superposition calculus is a calculus for reasoning in equational first-order logic.

Otter (theorem prover)

Otter
Otter, developed at the Argonne National Laboratory, is based on first-order resolution and paramodulation. Otter has since been replaced by Prover9, which is paired with Mace4.
Otter is an automated theorem prover developed by William McCune at Argonne National Laboratory in Illinois.

Prover9

Otter
Otter, developed at the Argonne National Laboratory, is based on first-order resolution and paramodulation. Otter has since been replaced by Prover9, which is paired with Mace4.
Prover9 is an automated theorem prover for First-order and equational logic developed by William McCune.

Vampire (theorem prover)

Vampire
Vampire is developed and implemented at Manchester University by Andrei Voronkov and Krystof Hoder, formerly also by Alexandre Riazanov. It has won the CADE ATP System Competition in the most prestigious CNF (MIX) division for eleven years (1999, 2001–2010).
Vampire is an automatic theorem prover for first-order classical logic developed in the School of Computer Science at the University of Manchester by Andrei Voronkov together with Kryštof Hoder and previously with Alexandre Riazanov.

SPASS

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.
SPASS is an automated theorem prover for first-order logic with equality developed at the Max Planck Institute for Computer Science and using the superposition calculus.

Rewriting

term rewritingterm rewriting systemrewrite system
Superposition and term rewriting
When combined with an appropriate algorithm, however, rewrite systems can be viewed as computer programs, and several theorem provers and declarative programming languages are based on term rewriting.

ACL2

ACL2 (A Computational Logic for Applicative Common Lisp) is a software system consisting of a programming language, an extensible theory in a first-order logic, and an automated theorem prover.

Models And Counter-Examples

MACE
Otter, developed at the Argonne National Laboratory, is based on first-order resolution and paramodulation. Otter has since been replaced by Prover9, which is paired with Mace4.
Most automated theorem provers try to perform a proof by refutation on the clause normal form of the proof problem, by showing that the combination of axioms and negated conjecture can never be simultaneously true, i.e. does not have a model.

PhoX

In automated theorem proving, PhoX is a proof assistant based on higher-order logic which is eXtensible.

SNARK (theorem prover)

SNARK
SNARK, (SRI's New Automated Reasoning Kit), is a theorem prover for multi-sorted first-order logic intended for applications in artificial intelligence and software engineering, developed at SRI International.

Prototype Verification System

PVS
Natarajan Shankar SRI International, work on decision procedures, little engines of proof, co-developer of PVS.
The Prototype Verification System (PVS) is a specification language integrated with support tools and an automated theorem prover, developed at the Computer Science Laboratory of SRI International in Menlo Park, California.

Well-formed formula

formulaformulaswell-formed
For a first order predicate calculus, 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.
Modern usages (especially in the context of computer science with mathematical software such as model checkers, automated theorem provers, interactive theorem provers) tend to retain of the notion of formula only the algebraic concept and to leave the question of well-formedness, i.e. of the concrete string representation of formulas (using this or that symbol for connectives and quantifiers, using this or that parenthesizing convention, using Polish or infix notation, etc.) as a mere notational problem.

Model elimination

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.
Their primary purpose is to carry out automated theorem proving, though they can readily be extended to logic programming, including the more general disjunctive logic programming.

Formal verification

program verificationverificationverified
One of the first fruitful areas was that of program verification whereby first-order theorem provers were applied to the problem of verifying the correctness of computer programs in languages such as Pascal, Ada, Java etc. Notable among early program verification systems was the Stanford Pascal Verifier developed by David Luckham at Stanford University.
Subareas of formal verification include deductive verification (see above), abstract interpretation, automated theorem proving, type systems, and lightweight formal methods.

EQP

EQP, an abbreviation for equational prover, is an automated theorem proving program for equational logic, developed by the Mathematics and Computer Science Division of the Argonne National Laboratory.

DPLL algorithm

DPLLDavis–Putnam–Logemann–Loveland algorithmDPLL solvers
DPLL
It has recently been extended for automated theorem proving for fragments of first-order logic.

Robbins algebra

Interactive provers are used for a variety of tasks, but even fully automatic systems have proved a number of interesting and hard theorems, including at least one that has eluded human mathematicians for a long time, namely the Robbins conjecture.
William McCune proved the conjecture in 1996, using the automated theorem prover EQP.