This survey paper is the first in a series of two issues of the Journal of Symbolic Computation dedicated to unification theory. It describes applications of unification in a wide variety of disciplines, recounts the early history of the field culminating in the crystallization of the fundamental problems in unification theory, and presents an exhaustive summary of basic results in the area.
The examples Siekmann gives as applications of unification theory demonstrate the usefulness of the techniques in various settings. Some of the examples are closely related, as when one field applies unification technology from another. For example, natural language processing applies unification theory through the use of unification in knowledge representation systems; similarly, computer algebra and automated theorem proving use it in equation solving and term rewriting systems. Some of the references in specific application areas could be updated. For example, in computer algebra, systems such as Milo and Mathematica rely much more heavily on pattern matching and unification than do Reduce and Macsyma. Siekmann’s point is well made, however: results from unification theory have useful applications in a wide variety of contexts.
Siekmann presents a self-contained basic introduction to the concepts of unification, matching, the set of most general unifiers of two terms, and the classification system for equational theories based on the cardinalities of sets of most general unifiers. He then organizes basic results from unification theory as they relate to the following problems concerning a given equational theory: determining the decidability of its unification problem, determining the possible cardinalities of sets of most general unifiers, and determining an efficient algorithm for computing a set of most general unifiers. Next, he presents these results for common first-order equational theories and gives the appropriate references. Siekmann also discusses the general combination problem for equational theories, sorted (typed) unification, higher-order unification, variable restricted unification, and the complexity relationship between the matching problem and the unification problem. The reader is directed to the appropriate references (which include other survey papers) for more detailed descriptions.
Siekmann also describes current approaches to a universal unification algorithm, that is, an algorithm to determine, given two terms and an equational theory, whether the terms are unifiable in the theory. Problems arise when equational theories on different function symbols are combined; these problems can be attacked using either narrowing or decomposition techniques. Siekmann points out how these general techniques have been used as starting places to develop improved unification algorithms in specific theories. Finally, he describes attempts to sharpen and refine the unification hierarchy through useful characteristics of equational theories (permutative, finite, simple, collapse-free, regular, and Noetherian theories) and presents some decidability results for these categories of equational theories.
The bibliography is split into two sections. The first lists papers of a more historical interest, which provide connections from unification theory to classical equation solving, logic, theorem proving, computer algebra, artificial intelligence, and other applications. The second presents references that contribute directly to the fundamental results that Siekmann summarizes in his overview of the progress of the field. Together, these bibliographies allow a reader who is new to unification theory to establish its relationships with other fields, and they provide useful pointers to the current literature.
Overall, Siekmann’s paper is a useful introduction to unification theory that clearly demonstrates the utility of unification to symbolic reasoning. As a survey paper, it also presents a coherent view of current results and research directions in the field and provides extensive bibliographic coverage of relevant papers.
