AUTOMATED THEOREM PROVING 17

functions were pursued by others such as Stickel [Stl] and Livesey

and Siekmann [LSl]. The paper· by Dallas J;.ankford in this volume

presents a unification algorithm for elementary Abelian groups. A

short survey of the research area {citing over ninety papers)

appears in [RS1]. Even before Plotkins' 1972 paper, Nevins had

incorporated some of these ideas in his theorem prover (see

[Ne1]) to handle some associative and commutative functions.

It

should be noted that special unification does not always yield a

single most general unifying substitution; indeed, there can be

infinitely many unifiers, and the unification algorithm may not

even be decidable.

The problem of unification of expressions has also been stu-

died for higher order logic, some notable papers in this area being

Gould [Go3], Huet [Hu1], and Jensen and Pietrzykowski [JP1].

Again, there may be one, finitely many or infinitely many unifiers.

The unification algorithm is undecidable, even for the subcase of

second-order logic (see Goldfarb [Go1]).

The advocates of the resolution approach have by no means

been quiescent during the 1970's. About 1972, the theorem prover

of Wos, Robinson and Carson was replaced by one developed by

Ross Overbeek. The system has continued to develop with contri-

butions from S. Winker, E. Lusk, B. Smith and L. Wos. The system

has been named AURA, for .A.Utomated .Reasoning Assistant. To

the mechanisms introduced in the 1960's (unit preference, set-of-

support for resolution; paramodulation and demodulation for han-

dling equalities), they have added hyperresolution, more flexibility

in demodulation, and preprocessors for preparation of input from

a variety of formats. They have done an extensive amount of

experimentation with the system, solving problems in circuit

design and program verification as well as formal logic and (finite)

mathematics. The result is a somewhat more human-oriented