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
Previous Page Next Page