Unification in a combination of arbitrary disjoint equational theories (Q582270)

The paper extends the known results on unification in a disjoint combination of regular and collapse-free equational theories (which are unification-type finitary) in the sense that arbitrary theories are admissible. The general procedure described is based on the reduction of the problem to the pure unification problem with free constants and the constant-elimination problem in the composing theories. It provides an enumeration of a complete set of unifiers, even if some unification procedure for a particular theory produces an infinite complete set of unifiers. It is proved that unifiability of \(E_ 1+E_ 2+...+E_ n\) is decidable if for every \(i=1,...,n\) there exists a method to decide unification in a combination of the \(E_ i's\) with free function symbols.