From: Dan Connolly <connolly@w3.org>

Date: Wed, 19 Jan 2000 16:56:51 -0600

Message-ID: <38864133.1C9AA573@w3.org>

To: sw99@w3.org

Date: Wed, 19 Jan 2000 16:56:51 -0600

Message-ID: <38864133.1C9AA573@w3.org>

To: sw99@w3.org

"Proofs found by programs are always questionable. Our approach to this problem is to have the theorem prover construct a detailed proof object and have a very simple program (written in a high-level language) check that the proof object is correct. The proof checking program is simple enough that it can be scrutinized by humans, and formal verification is probably feasible. EQP is not yet able to construct proof objects, so the EQP proof was used to guide Otter (using AC axioms instead of AC unification) to a proof of the same theorem. Otter produced a proof object, which was then checked by the proof checker. The input file, proof, proof object, Otter, and the proof checker are available: Otter Input Otter Proof Otter Proof Object Otter Source Code Proof Checker (requires Nqthm) " -- http://www-unix.mcs.anl.gov/~mccune/papers/robbins/ <-- http://www.cs.utexas.edu/users/boyer/ I gotta take a look at the proof checker... -- Dan Connolly http://www.w3.org/People/Connolly/Received on Wednesday, 19 January 2000 17:57:43 GMT

*
This archive was generated by hypermail 2.2.0
+ w3c-0.30
: Friday, 19 August 2005 11:10:28 GMT
*