Unification in a combination of arbitrary disjoint equational theories

The unification problem in a disjoint combination of equational theories, E1+...+En, is reduced to a combination of two kinds of problems in the Ej's: the pure unification, problem with free (Uninterpreted) constants and the constant-elimination problem. The constant-elimination problem is to find, given terms ti, 1≤i≤m and free constants ci, 1≤i≤m, all substitutions σ such that for all i with 1≤i≤m, σti is equal to some t′i that does not contain ci.The soundness and completeness of the method shows, that a disjoint combination of theories is finitary, provided every theory is finitary and constant-elimination problems in every theory are finitary solvable. In particular, any combination of finitary unifying regular theories, of Boolean rings, of Abelian groups or of theories with terminating basic narrowing, is of unification-type finitary. As a special case, unification in a combination of a free Boolean ring with free function symbols is decidable and finitary; the same holds for Abelian groups.This paper extends the known results on unification in a combination of regular and collapse-free theories in two aspects: i) Arbitrary theories are admissable. ii) The described general procedure can be used for enumerating a complete set of unifiers, even if some unification procedure for a paticular theory produces an infinite complete set of unifiers.It is demonstrated that unifiability of unification problems is decidable in the general case E1+...+En if for every i∈{1,…,n}, there is a method to decide unification problems in a combination of Ei with free function symbols