From owner-qed Mon Oct 31 09:21:37 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id JAA12443 for qed-out; Mon, 31 Oct 1994 09:21:14 -0600 Received: from mpi-sb.mpg.de (mpi-sb.mpg.de [139.19.1.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id JAA12437 for ; Mon, 31 Oct 1994 09:21:05 -0600 Organization: Max-Planck-Institut fuer Informatik D-66123 Saarbruecken, Germany Received: from mpii02006 with SMTP by mpi-sb.mpg.de (5.65/MPISB-1.0/920920) id AA20173; Mon, 31 Oct 94 16:20:52 +0100 Date: Mon, 31 Oct 94 16:20:49 +0100 Message-Id: <9410311520.AA10799@mpii02006.ag2.mpi-sb.mpg.de> Received: by mpii02006.ag2.mpi-sb.mpg.de; Mon, 31 Oct 94 16:20:49 +0100 From: Alan Bundy Subject: Machine verification of our proofs To: David McAllester In-Reply-To: David McAllester's message of Mon, 31 Oct 94 09:03:17 EST Phone: 49-681-302-5367 Fax: 49-681-302-5401 Fcc: +qed.mai Cc: qed@mcs.anl.gov Sender: owner-qed@mcs.anl.gov Precedence: bulk Dave McAllester writes: > I don't know of any papers published by system designers where an > important theorem about an inference mechanism, like a completeness > theorem, has been machine verified before publication. If we, the > most expert users, don't use them in our own mathematics how can we > expect other less formally oriented mathematicians to use them? I > think we have a long way to go. Absolutely! And this was even true when a machine checked proof would have been of real practical significance. Consider, for instance, all the controversy over the initial proofs of the paramodulation conjecture (that paramodulation was complete without the functional reflexive axioms). That issue would have been settled by a machine proof, but as far as I know, no-one even tried. Alan