English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/161159
Share/Impact:
Statistics
logo share SHARE logo core CORE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL
Exportar a otros formatos:
Title

On the undecidability of second-order unification

AuthorsLevy, Jordi ; Veanes, Margus
KeywordsLinear equations
Computational complexity
Unification
Problem solving
Issue Date2000
PublisherElsevier
CitationInformation and Computation 159: 125- 150 (2000)
AbstractThere 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 <n, (ii) the arity of all second-order variables is <n, (iii) the number of occurrences of second-order variables is ≤5, (iv) there is either a single second-order variable or there are two second-order variables and no first-order variables. © 2000 Academic Press.
URIhttp://hdl.handle.net/10261/161159
Identifiersdoi: 10.1006/inco.2000.2877
issn: 0890-5401
Appears in Collections:(IIIA) Artículos
Files in This Item:
File Description SizeFormat 
accesoRestringido.pdf15,38 kBAdobe PDFThumbnail
View/Open
Show full item record
Review this work
 

Related articles:


WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.