de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch

Hilfe Wegweiser Impressum Kontakt Einloggen

# Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

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

##### MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45662

Veanes,  Margus
Programming Logics, MPI for Informatics, Max Planck Society;

##### Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
##### Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
##### Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
##### Zitation

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

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.