Re: "explanations" in cwm, vocabulary for proof exchange

   [Sandro Hawke]
   Anyway, I've attached some demonstration runs below.  The output is
   IMHO quite hard to read (and I'm pretty comfortable with N3).   This
   is not an explanation for end-users yet, but I think we're more
   interested in proof exchange for machine consumption (verification)
   right now anyway.

   I know McGuinness et al have done some work in this area [1], and I'm
   hoping to coordinate with them more.  Is anyone else working in this
   area?

I've worked in this area occasionally, although not recently.  A few
years ago I supervised a Ph.D. thesis (never published, unfortunately)
on an interactive theorem prover, which, of course, could print out a
proof after one had been found.  (The author was Denys Duchier.)

We made two observations (certainly not original or earthshaking)
about machine-produced proofs:

1. Except for really trivial deductions, a machine-produced proof is
   usually not in the same form a person would produce.  Machines use
   formal frameworks that don't always match our intuitions, and they
   are happy when they reach the formal end of the proof process.
   For example, many theorem provers stop when they reach a
   contradiction, and a proof of "contradiction" from a dataset +
   negation of goal is pretty unenlightening.

2. The more the computer does for you, the harder it is to understand
   the printed proof.  That's because reading mathematical notations
   of any kind is just difficult.  If you had nothing to do with
   producing a proof, you're going to have to understand the proof
   from scratch.  It's tempting to just trust the machine.

Of course, neither observation applies to a machine checking a
machine-produced proof, which should be quite easy.

-- 
                                             -- Drew McDermott

Received on Friday, 25 April 2003 10:24:23 UTC