One-context Unification with STG-Compressed Terms is in NP

Carles Creus, Adria Gascón, Guillem Godoy

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

Abstract / Description of output

One context unification extends first-order unification by introducing a single context variable, possibly with multiple occurrences. One context unification is known to be in NP, but it is not known to be solvable in polynomial time. In this paper, we present a polynomial time algorithm for certain interesting classes of the one context unification problem. Our algorithm is presented as an inference system that non-trivially extends the usual inference rules for first-order unification. The algorithm is of independent value as it can be used, with slight modifications, to solve other problems, such as the first-order unification problem that tolerates one clash.
Original languageEnglish
Title of host publication23rd International Conference on Rewriting Techniques and Applications (RTA'12)
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Number of pages16
Publication statusPublished - 2012


Dive into the research topics of 'One-context Unification with STG-Compressed Terms is in NP'. Together they form a unique fingerprint.

Cite this