Automated theorem proving

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 well-developed 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 Co-NP-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 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 first-order 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
Well-order
Diophantine set
Lebesgue measure
Kolmogorov space
Laurent series
Banach fixed point theorem
Linear equation
Cartesian product
Linear
Axiom of regularity
Conjunctive normal form
Cardinality