History of Automated theorem proving

Difference (from prior major revision) (minor diff, author diff)

Changed: 3c3

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?.

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

Changed: 7c7,12

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.

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.

	Revision 5 . . (edit) November 24, 2001 2:04 am by (logged).109.194.xxx [typo]
	Revision 4 . . November 17, 2001 7:54 am by Cwitty [I don't think the four color theorem proof was model checking]
	Revision 3 . . November 17, 2001 6:57 am by AxelBoldt [fix link to 4 color theorem]
	Revision 2 . . November 17, 2001 6:25 am by The Anome [Mentioned 4 colour theorem]
	Revision 1 . . November 17, 2001 6:02 am by Cwitty [A new page on automated theorem proving]