Automated theorem proving
Automated theorem proving 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 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 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
Referenced By
Comp.sc. | Computer Science | Computer Sciences | Computer Scientists | Computer scientist | Computing science | E equational theorem prover | List of mathematical topics | List of mathematical topics (A-C) | List of mathematics topics | Otter theorem prover
|
