Equational unification, word unification, and 2nd-order equational unification

For finite convergent term-rewriting systems it is shown that the equational unification problem is recursively independent of the equational matching problem, the word matching problem, and the 2nd-order equational matching problem. Apart from the latter these results are derived by considering term-rewriting systems on signatures that contain unary function symbols only (i.e., string-rewriting systems). Also for this special case 2nd-order equational matching is shown to be reducible to Ist-order equational matching. In addition, we present some new decidability results for simultaneous equational matching and unification. Finally, we compare the word unification problem to the 2nd-order equational unification problem. (C) 1998-Elsevier Science B.V. All rights reserved.