Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures

Most of the work on the combination of unification algorithms for the union of disjoint equational theories has been restricted to algorithms that compute finite complete sets of unifiers.Thus the developed combination methods usually cannot be used to combine decision procedures,i.e., algorithms that just decide solvability of unification problems without computing unifiers.In this paper we describe a combination algorithm for decision procedures that works for arbitrary equational theories, provided that solvability of so–called unification problems with constant restrictions—a slight generalization of unification problems with constants—is decidable for these theories.As a consequence of this new method, we can, for example, show that generalA-unifiability, i.e.,solvabilityofA-unification problems with free function symbols, is decidable. HereAstandsfor the equational theory of one associative function symbol.Our method can also be used to combine algorithms that compute finite complete sets of unifiers. Manfred Schmidt–Schaußʹ combination result, the until now most general result in this direction, can be obtained as a consequence of this fact.We also obtain the new result that unification in the union of disjoint equational theories is finitary, if general unification—i.e., unification of terms with additional free function symbols—is finitary in the single theories.