Automated theorem proving

Automated theorem proving (also often called automated reasoning) is the proving of mathematical theorems by a computer program. It differs from automated proof verification: the proof verification problem is primitive recursive and has a very fast decision procedure; the set of theorems on the other hand, is undecidable -- at best only recursively enumerable.

In reality, there is no general-purpose system that can fully automatically prove "interesting" theorems, and most theorem proving systems can be used in a variety of ways with different amounts of automation, so this distinction is often dropped and both sides of the continuum are called theorem proving.

Another distinction is sometimes drawn between theorem proving and other techniques, where a process is considered to be theorem proving if it consists of a traditional proof, starting with axioms and producing new inference steps using rules of inference. Other techniques would include model checking, which is equivalent to brute-force enumeration of many possible states (although the actual implementation of model checkers requires much cleverness, and does not simply reduce to brute force). There are hybrid theorem proving systems which use model checking as an inference rule. There are also programs which were written to prove a particular theorem, with a (usually informal) proof that if the program finishes with a certain result, then the theorem is true. A good example of this was the machine-aided proof of the four color theorem, which was very controversial as the first claimed mathematical proof which was essentially impossible to check by hand. Another example would be the proof that the game Connect_Four is a win for the first player.

Commercial use of automated theorem proving is mostly concentrated in integrated circuit design and verification. Since the Pentium FDIV bug, the complicated floating point units of modern microprocessors have been designed with extra scrutiny. In the latest processors from AMD, Intel, and others, automated theorem proving has been used to verify that the divide and other operations are correct.

Popular techniques

Popular implementations

Some modern theorem provers:

You can find information on some of these theorem provers and others at http://www.cs.miami.edu/~tptp/CASC/19/SystemDescriptions.html

Important people