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