In the middle of the 1990s, a competition pitting automated theorem-proving systems against one another was started. However, several natural deduction theorem-proving systems have entered competitions over the last 15 years. 

The standard proof method used in computer-oriented automated proof systems is resolution. Some automated theorem-proving systems use natural deduction techniques. Still, some were "front-end programmes" that classified problems, broke them into more straightforward issues, and fed the simpler problems to standard resolution programmes. Although all resolution-based systems had first to convert the issues to clause form before beginning their proofs, they easily defeated MUSCADET.

Proof verification

Proof verification is a more straightforward but similar topic in which an existing proof for a theorem is certified legitimate. Generally, each proof step must be verifiable by a simple recursive function or programme, and the problem must always be decidable. Because the proofs created by automated theorem provers are often rather significant, the problem of proof compression is critical, and different strategies have been devised to make the prover's output smaller and, therefore, more easily intelligible and checkable. Proof helpers rely on human input to provide pointers to the machine. 

Interactive provers

Interactive provers are employed for a range of jobs. Still, even fully automatic systems have proven several intriguing and complex theorems, including at least one that has long escaped human mathematicians, the Robbins conjecture. However, these accomplishments are rare, and working on complex problems usually necessitates the employment of a skilled user.

Another contrast is made between theorem proving and other techniques, with a procedure regarded as a theorem, proving if it comprises a typical proof, beginning with axioms and constructing new inference steps using inference rules. Finally, model checking is another technique that, in its most basic form, employs brute-force enumeration of many possible states (however, the actual implementation of model checkers requires significant intelligence and does not simply reduce to brute force).

Problem decidability

Formula validity might be trivial or impossible, depending on the logic. For example, the frequent case of propositional logic is decidable but co-NP-complete. Therefore only exponential-time algorithms are assumed to exist for broad proving problems. On the other hand, Gödel's completeness theorem asserts that a first-order predicate calculus's theorems (provable propositions) are precisely the logically valid well-formed formulas. Hence discovering suitable formulae is recursively enumerable. Given limitless resources, every valid formula can be proven. However, faulty formulas—those not entailed by a theory—cannot consistently be recognised.

First-order theories

First-order theories like Peano arithmetic apply. However, a first-order theory may describe a model with true but undecidable propositions. By Gödel's incompleteness theorem, any idea whose proper axioms are valid for the natural numbers cannot prove all first-order propositions true for the natural numbers, even if the list is infinite. Even if the proposition being explored is true in the model of interest, an automated theorem prover will fail to terminate when searching for proof if the theory employed is undecidable. Nevertheless, theorem provers can solve many complex problems, even in models like the integers not fully characterised by any first-order theory, notwithstanding this theoretical limit.

Applications

Most of the market for automated theorem proving is in verifying integrated circuits. Since the Pentium FDIV flaw, modern microprocessors have been designed with greater care for their complex floating point units. As a result, automated theorem proving is used by AMD, Intel, and others to ensure that division and other operations are implemented correctly in their processors.

Image source: Unsplash