# Item

ITEM ACTIONSEXPORT

Released

Journal Article

#### On the Undecidability of Second-Order Unification

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

There are no public fulltexts stored in PuRe

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Levy, J., & Veanes, M. (2000). On the Undecidability of Second-Order Unification.* Information and Computation,* *159*, 125-150.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-344E-8

##### Abstract

There is a close relationship between word unification and second-order
unification. This similarity has been exploited, for instance, for proving
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 (non-linear) second-order
unification failed, and lead instead to a natural reduction from simultaneous
rigid E-unification to this problem. 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 \emph{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 conditions (i--iv) hold for some fixed integer $n$: (i) the
arguments of all second-order variables are ground terms of size less than $n$,
(ii) the arity of all second-order variables is less than $n$, (iii) the
number of occurrences of second-order variables is at most 5, (iv) there is
either a single second-order variable, or there are two second-order variables
and no first-order variables.