From lusk Fri Jun 17 08:23:33 1994
Received: from head.cs.wisc.edu (head.cs.wisc.edu [128.105.9.41]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id IAA10448 for <qed@mcs.anl.gov>; Fri, 17 Jun 1994 08:04:59 -0500
Date: Fri, 17 Jun 94 08:04:57 -0500
From: kunen@cs.wisc.edu (Ken Kunen)
Message-Id: <9406171304.AA19051@head.cs.wisc.edu>
Received: by head.cs.wisc.edu; Fri, 17 Jun 94 08:04:57 -0500
To: qed@mcs.anl.gov
Subject: Report on QED Workshop


Regarding the "Report on QED Workshop" by John Staples:

Good report!

On the benchmark examples:

>>   First example.  Prove from the following axioms of group theory:
>>       x(y.z) = (x.y).z
>>       x.1 = x
>>       x.i(x) = 1
>>   the theorem
>>       1.x = x


In this sort of purely equational reasoning, computers often outdo
humans; for example, Otter gets a proof  in < 1 second.
Otter's proof is somewhat shorter that the one quoted from Hall.

A word of caution when we go to sell this area to mathematicians:

I quote, without comment, from "Algebra" by I. Martin Isaacs
(Brooks/Cole 1994), where this result is Theorem 1.6:
    We should mention that the "elementwise" calculations in the
    preceding proof are not typical of most algebra.  The proof of
    Theorem 1.6, in fact, could almost serve as a model of what algebra
    is not, or at least should not be, in the opinion of the author.


Ken Kunen