Report on QED Workshop

Ken Kunen (
Fri, 17 Jun 94 08:04:57 -0500

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