A GENERALIZED APPROACH TO EQUATIONAL UNIFICATION
Kathy Yelick · DSpace@MIT (Massachusetts Institute of Technology) · 1985
Given a set of equational axioms and two terms containing function symbols and variables, the equational unification problem is to find a uniform replacement of terms for the variables that makes the terms provably equal from the axioms. In the general case, the two terms may contain symbols not appearing in the axioms, there may be more than one instance of a set of axioms, and there may be more than one set of axioms. This thesis presents a method for combining equational algorithms to handle the terms with mixed sets of function symbols. For example, given one algorithm for unifying associative-cummutative operators, and another for unifying commutative operators, the author's algorithm provides a method for unifying terms containing both kinds of operators. It is based on a general strategy for decomposing terms and combining unifiers. Attention is restricted to set of axioms whose function symbols are pairwise disjoint.