Machine verification of our proofs

Alan Bundy (bundy@mpi-sb.mpg.de)
Mon, 31 Oct 94 16:20:49 +0100

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