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