Combining Unification Algorithms

An algorithm is presented for solving equations in a combination of arbitrary theories over disjoint sets of function symbols. It is an extension of (Boudetel al. 1989) in which the problem was treated for the combination of an arbitrary and a simple theory. The algorithm consists of a set of transformation rules that simplify a unification problem until a solved form is obtained. Each rule is shown to preserve solutions, and solved problems are unification problems in normal form. The rules terminate for any control that delays replacement until the end. The algorithm is more efficient than Schmidt-Schauß (1990) because nondeterministic branching is performed only when necessary, that is when theory clashes or compound cycles are encountered. The results presented here come from the authorʹs thesis (Boudet (1990a)).