One Context Unification Problems Solvable in Polynomial Time

A. Gascon, A. Tiwari, M.S. Schaus

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


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 publicationLogic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages12
ISBN (Print)978-1-4799-8875-4
Publication statusPublished - 1 Jul 2015


  • computability
  • computational complexity
  • inference mechanisms
  • first-order unification
  • inference rules
  • inference system
  • one context unification problems
  • polynomial time algorithm
  • single context variable
  • Computer science
  • Context
  • Inference algorithms
  • Polynomials
  • Standards
  • Syntactics
  • Time measurement
  • Context Unification
  • Higher-order Unification
  • Polynomial-time
  • Term DAGs
  • Unification

Fingerprint Dive into the research topics of 'One Context Unification Problems Solvable in Polynomial Time'. Together they form a unique fingerprint.

Cite this