EQUATIONAL UNIFICATION, WORD UNIFICATION, AND 2ND-ORDER EQUATIONAL UNIFICATION

For finite convergent term-rewriting systems it is shown that the equa tional unification problem is recursively independent of the equationa l matching problem, the word matching problem, and the 2nd-order equat ional matching problem. Apart from the latter these results are derive d by considering term-rewriting systems on signatures that contain una ry function symbols only (i.e., string-rewriting systems). Also for th is special case 2nd-order equational matching is shown to be reducible to Ist-order equational matching. In addition, we present some new de cidability results for simultaneous equational matching and unificatio n. Finally, we compare the word unification problem to the 2nd-order e quational unification problem. (C) 1998-Elsevier Science B.V. All righ ts reserved.