A unification algorithm for simple theories
Mark Franzen · 1988
First studied in the context of resolution-based theorem provers,unification now plays an important role in many areas of computer science and artificial intelligence. Unification theory is concerned with the problem of solving equations in a variety, i.e. finding a substitution for the variables in two terms which makes them equal under a given set of axioms. Special unification procedures are known for several equational theories. However, most of these procedures are based on entirely different methods--methods specific to the theory. In this thesis, an algorithm is presented which solves the unification problem for a wide class of theories. The method is based on variable abstraction and requires that a special set of unifiers be known for the given theory. The algorithm is partially correct for simple theories and a stronger result shows that the algorithm is complete for any theory which is subterm Noetherian--a slightly narrower class than the simple theories. In addition, it is shown that the special set needed to start the procedure can be generated automatically for certain theories.