16

D.W. LOVELAND

of equational theories permit computation of a complete set of

rewrite rules; that is, a set of rewrite rules sufficient to check the

truth of every equation of the tpeory by demand.ing that equal

terms reduce to the same normal form. The theory of groups is

one such theory while the theory of abelian groups is not. How-

ever, the problems of handling commutativity (and similar prob-

lems with associativity within some equational theories) have been

surmounted in limited cases by researchers such as Lankford and

Ballantyne, Huet and Peterson, Slagle, and Stickel. (For example,

see [Sl2],

[LBl].

[Hu2], [PSl].) A key idea here has been the use of

auxiliary equivalence classes; for example, one equatc;:s terms that

reduce to terms within the same equivalence class. An

unanswered question was (and is): what equational theories have

complete sets of rewrite rules? One faces both the problems of

finite termination of a sequence of .terms under rewrite transfor-

mations and, if termination occurs, whether a normal form is

reached whenever it should be. This problem has been investi-

gated by a number of people (see Huet and Oppen [HOl] for a

technical overview). This approach has been integrated with reso-

lution (see Slagle [Sll],[Sl2]).

A research area very close to rewrite (or reduction) systems is

that of special unification algorithms. As previously mentioned,

unification is the name J.A. Robinson gave to the process for

finding a most general substitution for variables to make atomic

formulas identical. Special unification also seeks to "unify"

atomic formulas, but within special theories, usually equational

theories. The usual unification process is augmented by equations

or rewrite rules in such a manner as to make unnecessary the

explicit listing of the equations as axioms. This idea was first for-

malized in Plotkin [Pl2] to deal with general equational theories.

Equational theories with commutative and/or associative