压缩项的统一与匹配
Unification and Matching on Compressed Terms
摘要：
术语统一在计算机科学的许多领域中起着重要的作用，特别是在与逻辑相关的领域中。基于语法的术语压缩的通用机制，特别是所谓的单例树语法（STG），最近引起了相当大的关注。使用STG，指数大小和高度的项可以在线性空间中表示。此外，术语表示的有向无环图（dags）可以有效地模拟。本文件是长期统一和匹配时，作为输入的条款表示使用不同的压缩机制，如dags和单例树文法的调查结果。我们描述了一个多项式时间算法的上下文匹配dags，当不同的上下文变量的数量是固定的问题。对于同样的问题，NP-完全时，条款表示使用更一般的形式主义的单例树文法。对于一阶统一和匹配问题，给出了多项式时间算法，改进了已有的结果。
英文摘要：
Term unification plays an important role in many areas of computer science, especially in those related to logic. The universal mechanism of grammar-based compression for terms, in particular the so-called Singleton Tree Grammars (STG), have recently drawn considerable attention. Using STGs, terms of exponential size and height can be represented in linear space. Furthermore, the term representation by directed acyclic graphs (dags) can be efficiently simulated. The present paper is the result of an investigation on term unification and matching when the terms given as input are represented using different compression mechanisms for terms such as dags and Singleton Tree Grammars. We describe a polynomial time algorithm for context matching with dags, when the number of different context variables is fixed for the problem. For the same problem, NP-completeness is obtained when the terms are represented using the more general formalism of Singleton Tree Grammars. For first-order unification and matching polynomial time algorithms are presented, each of them improving previous results for those problems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
