License:
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.405
URN: urn:nbn:de:0030-drops-54289
URL: https://drops.dagstuhl.de/opus/volltexte/2015/5428/
Gascón, Adrià ;
Schmidt-Schauß, Manfred ;
Tiwari, Ashish
Two-Restricted One Context Unification is in Polynomial Time
Abstract
One Context Unification (1CU) extends first-order unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several more-general classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of first-order unification and can be used to solve related problems in polynomial time, such as first-order unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs.
BibTeX - Entry
@InProceedings{gascn_et_al:LIPIcs:2015:5428,
author = {Adri{\`a} Gasc{\'o}n and Manfred Schmidt-Schau{\ss} and Ashish Tiwari},
title = {{Two-Restricted One Context Unification is in Polynomial Time}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {405--422},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Stephan Kreutzer},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5428},
URN = {urn:nbn:de:0030-drops-54289},
doi = {10.4230/LIPIcs.CSL.2015.405},
annote = {Keywords: context unification, first-order unification, deduction, type checking}
}
Keywords: |
|
context unification, first-order unification, deduction, type checking |
Collection: |
|
24th EACSL Annual Conference on Computer Science Logic (CSL 2015) |
Issue Date: |
|
2015 |
Date of publication: |
|
07.09.2015 |