AUTOMATED THEOREM PROVING

15

An independent but parallel effort in human oriented theorem

proving was undertaken about the same time by Arthur Nevins,

then at George Washington University [Nel,Ne2,Ne3]. Nevins built

at least two provers; he received considerable attention for the

ability of hi::; provers to prove theorems which most resolution

provers could not touch and was at the then outer limit of the

prover of Wos et al. For example, Nevins could prove, fully

automatically, z

3

=

e

=

I(!

(a,b ),b)

=

e

where

f

(z,y)

=

zyz-ly-1,

a result considerably harder than the

"z

2

=

e

==

the

group

is abelian" proved (with guidance) by

Norton with ADEPT. (A considerably more efficient automatic

proof of this theorem was accomplished using the method of

rewrite rules (see below) using an improvement due to Lankford.

See

[Bll].)

Not all the activity and new ideas of 1970 were on the human

simulation side of theorem proving. In 1970 Knuth and Bendix

published a paper (see [KB1]) that refocussed the attention of

many theoreticians in ATP on the potential of rewrite rules, a dev-

ice familiar to logicians. (Effectively, the use of rewrite rules in

ATP had been underway for several years by Wos via demodula-

tion.) A rewrite rule is a replacement rule, usually written so that

the left hand side is replaceable by the right hand side at any

occurrence of the left hand side, aft-er variable substitution. For

example, z

+

(-z)= 0 is a rewrite rule of arithmetic; such rewrite

rules that simplify an expression are called simplification rules.

In equational theories, one converts equations to rewrite rules

(primarily by choosing a direction for rewriting). Then one can

repeatedly rewrite (reduce) terms via rewrite rules and equate

terms that reduce to the same term (their "normal form") via

~ewrite

rules. Knuth and Bendix gave an algorithm that for a class