There is a close relationship between word unification and second-order unification. This similarity has been exploited, for instance, in order to prove decidability of monadic second-order unification and decidability of linear second-order unification when no second-order variable occurs more than twice. The attempt to prove the second result for (nonlinear) second-order unification failed and led instead to a natural reduction from simultaneous rigid E-unification to this second-order unification. This reduction is the first main result of this paper, and it is the starting point for proving some novel results about the undecidability of second-order unification presented in the rest of the paper. We prove that second-order unification is undecidable in the following three cases: (1) each second-order variable occurs at most twice and there are only two second-order variables; (2) there is only one second-order variable and it is unary; (3) the following conditions (i)-(iv) hold for some fixed integer n: (i) the arguments of all second-order variables are ground terms of size

This work was partially supported by Project MODELOGOS (TIC97-0579-C02-01) funded by the CICYT, and the ESPRIT Basic Research Action CCL. This paper is based on preliminary results in (Levy, 1998; Veanes, 1998; Levy and Veanes, 1998). The second author worked at Max-Planck-Institute of Computer Science, Saarbruecken, Germany, when this paper was submitted.

Peer Reviewed