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:
“Will women find themselves in the same position they have always been? Or do we see liberation as solving the conditions of women in our society?... If we continue to shy away from this problem we will not be able to solve it after independence. But if we can say that our first priority is the emancipation of women, we will become free as members of an oppressed community.”
—Ruth Mompati (b. 1925)