algorithm - 叠加微积分和方程的排序

Question

叠加演算是一种定理证明技术，它通过施加约简排序而不是在两个方向上应用每个方程来降低副调制的多产性。

对于一个非常简单的测试用例，请考虑以下子句(使用小写字母表示常量而不是变量的符号):

a=b
a=c
b!=c

显然，应该可以从这些条款中推断出矛盾。

在这种情况下，我们只有基原子项的单位子句，因此叠加规则可以用大大简化的形式来表述。

叠加，左:

s=t, s!=v => t!=v

其中 s > t，t >= v 在所选的归约排序中。 (完整版本的叠加需要将子句作为文字的多集处理，使用变量替换，并使用仅在基本项上合计的归约排序，但这些不适用于此处讨论的简单测试用例。)

同样，

叠加，右:

s=t, s=v => t=v

其中 s > t，t >= v 在所选的归约排序中。

假设我们使用归约排序 a > b > c。然后:

a=b, a=c => b=c
b=c, b!=c => false

但是，对于任何归约排序的选择，演算都需要完备。假设 c > b > a，则上面的第一个推论是不允许的。

候选备选推理:

c=a, c!=b => a=b

也不允许，因为 b > a。

替代版本:

c=a, c!=b => b=a

这需要在归约顺序允许的方向上尝试输入方程，然后翻转输出方程以同样匹配归约顺序。当您这样做时，它会起作用。

这是允许的吗？换句话说，叠加微积分定义的意图是，方程是无序的，所以每个方程的产生和使用都应该以与归约顺序相匹配的顺序进行？

Answer 1

仅作记录:在叠加微积分的标准理论阐述中(我的 goto 论文是 Leo Bachmair 和 Harald Ganzinger，“基于重写的方程式定理证明与选择和简化”，逻辑与计算杂志，1994 年， 3(4):217-247)，所有文字都是方程式或不等式。这些要么明确定义为无序对，然后在多重集编码中进行比较，要么直接定义为多重集(具体细节取决于您阅读的论文，但这些大多只是对同一基本概念的不同描述)。

是的，您关于方程式无序的假设是正确的。我所知道的所有实现本质上都是定向的，因此需要明确考虑与术语排序兼容的所有方向。