Journal Article @Article Artikel in Fachzeitschrift
 Show entries of: this year (2019) | last year (2018) | two years ago (2017) | Notes URL
 Action: login to update Options: Goto entry point

 Author, Editor(s)
 Author(s): Levy, Jordi Veanes, Margus dblp dblp
 BibTeX cite key*: LevyVeanes99

 Title
 Title*: On the Undecidability of Second-Order Unification

 Journal

 Publisher
 Publisher's Name: Academic Press Publisher's URL: http://www.apnet.com/ Publisher's Address: London, UK ISSN: 0890-5401

 Vol, No, pp, Date
 Volume*: 159 Number: Publishing Date: 2000 Pages*: 125-150 Number of VG Pages: Page Start: Page End: Sequence Number: DOI:

 Note: (LaTeX) 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. URL for the Abstract: Categories, Keywords: Second-Order Unification HyperLinks / References / URLs: Copyright Message: Personal Comments: Download Access Level:

 Correlation
 MPG Unit: Max-Planck-Institut für Informatik MPG Subunit: Programming Logics Group Audience: experts only Appearance: MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat

BibTeX Entry:

@ARTICLE{LevyVeanes99,
AUTHOR = {Levy, Jordi and Veanes, Margus},
TITLE = {On the Undecidability of Second-Order Unification},
JOURNAL = {Information and Computation},