Unification in combinations of collapse-free regular theories (Q1099652)

This paper presents a method for combining equational unification algorithms to handle terms containing `mixed' sets of function symbols. For example, given one algorithm for unifying associative-commutative operators, and another for unifying commutative operators, our algorithm provides a method for unifying terms containing both kinds of operators. As a special case of the combining problem, our algorithm lifts a variable-only case algorithm to the general case with multiple operator instances and free symbols. We restrict our attention to a class of equational theories called the collapse-free regular theories. We give some results characterizing the unification problem in this class of theories, and specifically show the restrictions are necessary and sufficient for the correctness of our algorithm. An implementation has been done as part of a large system for reasoning about equational theories.