Unification in a combination of equational theories: An efficient algorithm

Abstract

An algorithm is presented for solving equations in a combination of arbitrary theories with disjoint sets of function symbols. It is an extension of [3] in which the problem was treated for the combination of an arbitrary and a simple theory. The algorithm consists in 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 [13] because nondeterministic branching is performed only when necessary, that is when theory clashes or compound cycles are encountered.