
related topics 
{math, number, function} 
{system, computer, user} 
{theory, work, human} 
{game, team, player} 
{style, bgcolor, rowspan} 

Automated theorem proving (ATP) or automated deduction, currently the most welldeveloped subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program.
Contents
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 CoNPcomplete, and hence only exponentialtime 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 wellformed 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 firstorder 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
Full article ▸


related documents 
Mersenne twister 
Golomb coding 
Euler's totient function 
Symmetric group 
Controllability 
Kruskal's algorithm 
Convex set 
Search algorithm 
Local ring 
Constant of integration 
Exact sequence 
Mersenne prime 
Analytic geometry 
Group representation 
Carmichael number 
Goodstein's theorem 
Separable space 
Probability space 
Wellorder 
Diophantine set 
Lebesgue measure 
Kolmogorov space 
Laurent series 
Banach fixed point theorem 
Linear equation 
Cartesian product 
Linear 
Axiom of regularity 
Conjunctive normal form 
Cardinality 
