Almost every automated deduction system relies on unification in one form or another. Since the early 1960s, many implementations of unification have been produced in the field of automated deduction, from artificial intelligence to formal verification of computer programs to new paradigms for programming languages such as logic programming. Logic programming has been getting all the attention lately, because it also offers a popular programming language, Prolog, for readily implementing applications of automated deduction.

Standard term unification, such as that used in Prolog, is a simple but powerful procedure that determines whether two given terms, consisting of uninterpreted function symbols and variables, can be made identical by finding substitutions for the variables in these terms. Whenever such unifying substitutions, called unifiers, exist, a unique most general unifier from which all other unifying substitutions can be generated always exists. More recently, the need for two generalizations of ordinary term unification has emerged in the field of automated deduction. The first generalization calls for the incorporation of equality into theorem proving procedures, and the second calls for the automation of higher-order reasoning.

The main subject of this book is the detailed examination of what it means for two terms to become equivalent after application of a unifying substitution by a generalized unification. As part of this examination, many theoretical problems have to be addressed. Some of these problems are related to the fundamental mathematical properties of the unification procedure, such as termination and completeness. Other problems are caused by the practical considerations of computational feasibility and efficiency.

The book reports the results of the theoretical study of two generalizations of unification using an extension of the simple formalism developed for standard term unification. The author’s idea is to study unification as a nondeterministic procedure transforming a system of equations. This approach, which has some similarities to Gaussian elimination in linear algebra, provides an elegant abstract algebraic method of studying unification in various forms of generalization. For example, using the method, the author is able to prove the completeness of a general unification for first-order logic with equality. In addition, he is able to derive a number of new and important properties of the higher-order unifications.

The book’s greatest contribution is in providing a clear and rigorous framework for proving the basic properties of general unification. By presenting the unification process as a set of basic abstract transformations, the author is able to clearly identify the logically invariant properties of first-order unification and higher-order unification. The first few chapters provide a comprehensive introduction to the proof theory for general unification, including a detailed reformulation of standard term unification via transformations on the systems of equations. The definitions and results introduced by the initial chapters form the clear background for the major results derived for first-order unification and higher-order unification within the theory in the later chapters.

On the negative side, the author has, in his search for the purest declarative representation of unification, completely abandoned the discussion of the operational aspects of unification algorithms. Perhaps a discussion of various computational issues arising from the application of unification to automated deduction should be left to another monograph.

This book constitutes a major contribution to the formulation of a proof theory for general unification. Its presentation of recent developments is much more refined and theoretically complete than that of many existing surveys and research papers on general unification, most of which are cited in the extensive bibliography. Practitioners and students in automated deduction, artificial intelligence, and the theory of programming languages should find this work a most valuable reference on theoretical aspects of unification in their work and study.