关于破坏性等价解析在超位置计算中的(不)完备性

Bachmair 和 Ganzinger 的抽象冗余概念为超位置计算中的大多数操作提供了正当性，这些操作用于删除或简化子句，从而保持子句集的可管理性。典型例子包括恒等式删除、子sumption 删除和解码化，以及通过对冗余性的更精细定义，涵盖连接性和可达性。值得注意的例外是破坏性等价解析，即将子句 $x \not\approx t \lor C$（其中 $x \notin \mathrm{vars}(t)$）替换为 $C\{x \mapsto t\}$。该操作在当前先进的证明器中实现，并且在实际中明显有用，但关于其对参考完备性的影响几乎没有研究。我们一方面演示了，将破坏性等价解析的朴素添加方式引入标准抽象冗余概念后，使得该计算不再参考完备。另一方面，我们提出了几种受限制的超位置计算变体，即使包含破坏性等价解析也能保持参考完备性。