W3C home > Mailing lists > Public > sw99@w3.org > January to March 2000

more proof checking goodies...

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
"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

     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
Received on Wednesday, 19 January 2000 17:57:43 UTC

This archive was generated by hypermail 2.4.0 : Friday, 25 March 2022 10:06:24 UTC