ALGORITHM FOR UNIFICATION IN EQUATIONAL THEORIES

The paper presents a nondeterministic algorithm for unifying pairs of terms in equational theories consisting of a confluent and terminating set of rewrite rules. The algorithm, which can be considered a generalization of the standard unification algorithm by Martelli and Montanari, is described by means of transformations applied to sets of equations and is shown to be correct and complete. Another version of the algorithm, accepting also cyclic terms, is given for sets of multiequations. This algorithm is characterized by an outermost reduction strategy which permits dealing with infinite data structures. The algorithm can also be used as an interpreter for logic languages, thus providing a framework for trying to achieve the amalgamation of logic and functional languages.