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.
Read more about this topic: Automated Theorem Proving
Famous quotes containing the word problem:
“The government is huge, stupid, greedy and makes nosy, officious and dangerous intrusions into the smallest corners of life—this much we can stand. But the real problem is that government is boring. We could cure or mitigate the other ills Washington visits on us if we could only bring ourselves to pay attention to Washington itself. But we cannot.”
—P.J. (Patrick Jake)