Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








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

Journal Title*:

Information and Computation
Journal's URL:

http://www.academicpress.com/i&c

Download URL
for the article:


Language:

English

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, Abstract, ©

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},
 PUBLISHER = {Academic Press},
 YEAR = {2000},
 VOLUME = {159},
 PAGES = {125--150},
 ADDRESS = {London, UK},
 ISBN = {0890-5401},
}

Entry last modified by Christine Kiesel, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Margus Veanes		Created
04/22/1999 08:39:40 PM
Revisions
10.
9.
8.
7.
6.		Editor(s)
Christine Kiesel
Uwe Brahm
Uwe Brahm
Uwe Brahm
Uwe Brahm		Edit Dates
04.09.2001 11:19:29
04/04/2001 06:29:31 PM
04/04/2001 06:28:48 PM
04/04/2001 05:32:10 PM
14.03.2001 13:42:45