Editing Automated theorem proving (section)

== Decidability of the problem ==
{{Unreferenced section|date=April 2010}}
Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the common case of [[propositional logic]], the problem is decidable but [[co-NP-complete]], and hence only [[exponential time|exponential-time]] algorithms are believed to exist for general proof tasks. For a [[first-order logic|first-order predicate calculus]], [[Gödel's completeness theorem]] states that the theorems (provable statements) are exactly the semantically valid [[well-formed formula]]s, so the valid formulas are [[computably 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.

The above applies to first-order theories, such as [[Peano axioms|Peano arithmetic]]. However, for a specific model that may be described by a first-order theory, some statements may be true but undecidable in the theory used to describe the model. For example, by [[Gödel's incompleteness theorem]], we know that any consistent theory whose axioms are true for the natural numbers cannot prove all first-order statements true for the natural numbers, even if the list of axioms is allowed to be infinite enumerable. It follows that an automated theorem prover will fail to terminate while searching for a proof precisely when the statement being investigated is undecidable in the theory being used, even if it is true in the model of interest. Despite this theoretical limit, in practice, theorem provers can solve many hard problems, even in models that are not fully described by any first-order theory (such as the [[integer]]s).