- From: Drew McDermott <drew.mcdermott@yale.edu>
- Date: Fri, 25 Apr 2003 10:24:18 -0400 (EDT)
- To: www-rdf-logic@w3.org
[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