Unification, a fundamental operation in computer science and mathematics, has been studied in a wide variety of settings in recent years. This paper makes a significant contribution to unification theory by studying a particular kind of E-unification problem, namely, E-unification primal algebras, a class of finite algebras in which every function on the carrier can be expressed as a composition of the basic operations (for example, the Boolean algebra on {T,F} with operations ¬ and ∧ is primal). The approach taken is to extend the author’s previous work with Martin on Boolean unification to arbitrary varieties generated by primal algebras. For the computer scientist, these unification problems are particularly important in that they are decidable (albeit NP-complete) and that when solutions exist, a most general unifier always exists, as in standard unification; this makes implementation of the overall deduction system much simpler. Unification in primal algebras (in the simple case of Boolean algebras) has been used to augment Prolog for the purpose of hardware verification, but promises in the future to be useful in reasoning about various paradigms in computer science, from many-valued logics to modular arithmetic.

This theoretical work is well written and rigorous, but it presupposes a fair amount of algebraic maturity on the part of the reader. Although complexity issues are discussed, no practical experience with these algorithms is presented. The author makes a solid contribution to the theory of unification in a setting that could prove to be of significant practical import for automated reasoning about various kinds of logic (including digital logic). This paper should be of interest not only to theoreticians but also to researchers in computer algebra, automated theorem proving, and logic programming.