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

Authors Carles Creus, Adria Gascon, Guillem Godoy

Thumbnail PDF


  • Filesize: 0.53 MB
  • 16 pages

Document Identifiers

Author Details

Carles Creus
Adria Gascon
Guillem Godoy

Cite AsGet BibTex

Carles Creus, Adria Gascon, and Guillem Godoy. One-context Unification with STG-Compressed Terms is in NP. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 149-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


One-context unification is an extension of first-order term unification in which a variable of arity one standing for a context may occur in the input terms. This problem arises in areas like program analysis, term rewriting and XML processing and is known to be solvable in nondeterministic polynomial time. We prove that this problem can be solved in nondeterministic polynomial time also when the input is compressed using Singleton Tree Grammars (STG's). STG's are a grammar-based compression method for terms that generalizes the directed acyclic graph representation. They have been recently considered as an efficient in-memory representation for large terms, since several operations on terms can be performed efficiently on their STG representation without a prior decompression.
  • Term Unification
  • Compression
  • Grammars


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail