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

From: Drew McDermott <drew.mcdermott@yale.edu>
Date: Fri, 25 Apr 2003 10:24:18 -0400 (EDT)
Message-Id: <200304251424.h3PEOIl15326@pantheon-po02.its.yale.edu>

```

[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)

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

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:52:43 GMT