2026-07-24T18:04:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3490 2024-03-06T10:34:17Z ddc:004 open_access

One-context Unification with STG-Compressed Terms is in NP Creus, Carles Gascon, Adria Godoy, Guillem Term Unification Compression Grammars 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Carles Creus and Adria Gascon and Guillem Godoy 2012 Is Part Of LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2012.149 urn:nbn:de:0030-drops-34902 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.149 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode