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