论叠加演算中破坏性等式消解的不完全性
On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus
AI总结：
本文研究叠加演算中破坏性等式消解对反驳完全性的影响，证明直接加入该操作会导致不完全性，并提出若干保持反驳完全性的受限演算变体。
摘要：
Bachmair和Ganzinger为叠加演算提出的抽象冗余概念，几乎为叠加证明器中用于删除或化简子句、从而保持子句集可管理的所有操作提供了正当性。典型例子包括重言式删除、包含删除和解调，并且借助更精细的冗余定义，可连接性和连通性也能被覆盖。显著的例外是破坏性等式消解，即将满足$x \notin \mathrm{vars}(t)$的子句$x \not\approx t \lor C$替换为$C\{x \mapsto t\}$。该操作已在最先进的证明器中实现，并且在实践中明显有用，但关于它如何影响反驳完全性却鲜为人知。我们一方面证明，将破坏性等式消解直接加入标准抽象冗余概念会使演算变得反驳不完全。另一方面，我们给出了叠加演算的若干受限变体，这些变体即使加入破坏性等式消解也仍然反驳完全。
英文摘要：
Bachmair's and Ganzinger's abstract redundancy concept for the Superposition Calculus justifies almost all operations that are used in superposition provers to delete or simplify clauses, and thus to keep the clause set manageable. Typical examples are tautology deletion, subsumption deletion, and demodulation, and with a more refined definition of redundancy joinability and connectedness can be covered as well. The notable exception is Destructive Equality Resolution, that is, the replacement of a clause $x \not\approx t \lor C$ with $x \notin \mathrm{vars}(t)$ by $C\{x \mapsto t\}$. This operation is implemented in state-of-the-art provers, and it is clearly useful in practice, but little is known about how it affects refutational completeness. We demonstrate on the one hand that the naive addition of Destructive Equality Resolution to the standard abstract redundancy concept renders the calculus refutationally incomplete. On the other hand, we present several restricted variants of the Superposition Calculus that are refutationally complete even with Destructive Equality Resolution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
