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

AbstractFor 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 1st-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