[4] Russell and Whitehead thought they could derive all mathematical truth using axioms and inference rules of formal logic, in principle opening up the process to automation.
In 1954, Martin Davis programmed Presburger's algorithm for a JOHNNIAC vacuum-tube computer at the Institute for Advanced Study in Princeton, New Jersey.
[7] The "heuristic" approach of the Logic Theorist tried to emulate human mathematicians, and could not guarantee that a proof could be found for every valid theorem even in principle.
For the common 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.
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 integers).
For this, it is generally required that each individual proof step can be verified by a primitive recursive function or program, and hence the problem is always decidable.
Interactive provers are used for a variety of tasks, but even fully automatic systems have proved a number of interesting and hard theorems, including at least one that has eluded human mathematicians for a long time, namely the Robbins conjecture.
Since the Pentium FDIV bug, the complicated floating point units of modern microprocessors have been designed with extra scrutiny.
AMD, Intel and others use automated theorem proving to verify that division and other operations are correctly implemented in their processors.
[14] Applications of theorem provers are also found in natural language processing and formal semantics, where they are used to analyze discourse representations.
[15][16] In the late 1960s agencies funding research in automated deduction began to emphasize the need for practical applications.
On the other hand, it is still semi-decidable, and a number of sound and complete calculi have been developed, enabling fully automated systems.