不对称统一与不统一
Asymmetric Unification and Disunification
摘要：
我们比较了两类统一问题：非对称统一和不统一，它们是等式统一的变体。非对称统一是一种方程统一，其中方程的右侧相对于给定项重写系统为范式。在Disunification我们解决方程和disequations相对于一个方程理论的情况下，自由常数。我们对比了两者的时间复杂度，并表明这两个问题是不可比拟的：有一些理论，其中一个可以在多项式时间内求解，而另一个则是NP难的。这是双向的时间复杂度还基于术语重写系统中使用的终止排序而变化。
英文摘要：
We compare two kinds of unification problems: Asymmetric Unification and Disunification, which are variants of Equational Unification. Asymmetric Unification is a type of Equational Unification where the right-hand sides of the equations are in normal form with respect to the given term rewriting system. In Disunification we solve equations and disequations with respect to an equational theory for the case with free constants. We contrast the time complexities of both and show that the two problems are incomparable: there are theories where one can be solved in Polynomial time while the other is NP-hard. This goes both ways. The time complexity also varies based on the termination ordering used in the term rewriting system.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
