最通用的变体统一符
Most General Variant Unifiers
摘要：
两项的等式统一包括找到一个替换，当应用于两项时，使它们在某些等式属性的模上相等。方程统一是特别相关的自动演绎，定理证明，协议分析，部分评估，模型检验，等几个算法已经在文献中开发的具体方程理论，如关联交换符号，异或，Diffie-Hellman，或阿贝尔群。缩小被证明是完整的统一和几种情况下已经研究了缩小提供了一个可判定的统一算法。一个新的基于窄化的方程统一算法依赖于一个术语的变体的概念已经开发出来，它是在最新版本的Maude，版本2.7.1，它提供了相当复杂的统一功能。项t的变体是由替换σ和tsigma的标准形式组成的对。当方程理论满足有限变分性质时，基于变分的统一是可判定的。然而，它可能会计算更多的统一比必要的，在本文中，我们将探讨如何加强基于变量的统一算法实现Maude产生一个最小的最一般的变量统一。我们的实验表明，这种新的适应的变量为基础的统一是更有效的执行时间和计算的变量统一比原始算法在Maude。
英文摘要：
Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. Equational unification is of special relevance to automated deduction, theorem proving, protocol analysis, partial evaluation, model checking, etc. Several algorithms have been developed in the literature for specific equational theories, such as associative-commutative symbols, exclusive-or, Diffie-Hellman, or Abelian Groups. Narrowing was proved to be complete for unification and several cases have been studied where narrowing provides a decidable unification algorithm. A new narrowing-based equational unification algorithm relying on the concept of the variants of a term has been developed and it is available in the most recent version of Maude, version 2.7.1, which provides quite sophisticated unification features. A variant of a term t is a pair consisting of a substitution sigma and the canonical form of tsigma. Variant-based unification is decidable when the equational theory satisfies the finite variant property. However, it may compute many more unifiers than the necessary and, in this paper, we explore how to strengthen the variant-based unification algorithm implemented in Maude to produce a minimal set of most general variant unifiers. Our experiments suggest that this new adaptation of the variant-based unification is more efficient both in execution time and in the number of computed variant unifiers than the original algorithm available in Maude.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
