Two-Restricted One Context Unification is in Polynomial Time

Adrià Gascon, Manfred Schmidt-Schauß, Ashish Tiwari

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publication24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Number of pages18
ISBN (Print)978-3-939897-90-3
Publication statusPublished - 2015

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
ISSN (Print)1868-8969


Dive into the research topics of 'Two-Restricted One Context Unification is in Polynomial Time'. Together they form a unique fingerprint.

Cite this