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.

There are many automated therem proving systems. Some of the more notable freely available systems include (in no particular order) HOL, Isabelle?, NuPRL?, MetaPRL?, Coq?, Mizar, ACL2?, and PVS?.

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 [model checking]?. Here, 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. Model checking uses other techniques, 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). A good example of this was the machine-aided proof of the four color theorem. There are hybrid theorem proving systems which use model checking as an inference rule.

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 unit]?s 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.