Automated theorem proving

Automated theorem proving is the process of getting a computer to agree that a particular theorem is true. The theorems of interest may be in traditional mathematical domains, or they may be in other fields such as digital computer design.

Sometimes a distinction is made between theorem-proving and proof verification. This distinction is about the degree of automation in the process. If a human writes a highly detailed step-by-step proof, and the computer merely checks each step, that would be called proof verification. On the other hand, if a human merely states the theorem to be proved, and the computer comes up with all necessary lemmas and the entire proof, that would be theorem proving. 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 4 is a win for the first player.

Commercial use of automated theorem proving is mostly concentrated in integrated circuit design and verification. Since the infamous 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.

Some popular theorem provers are: Isabelle, HOL, ACL2, PVS[?], Simplify[?], Otter[?], Vampire[?], Waldmeister[?], SPASS[?], Gandalf, NuPRL[?], MetaPRL[?], Coq[?], Mizar.