- From: Dan Connolly <connolly@w3.org>
- Date: Wed, 19 Jan 2000 16:56:51 -0600
- 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 UTC