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: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5428/
Go to the corresponding LIPIcs Volume Portal

Gascón, Adrià ; Schmidt-Schauß, Manfred ; Tiwari, Ashish

Two-Restricted One Context Unification is in Polynomial Time

pdf-format:
25.pdf (0.6 MB)

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI