On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus
CoRR(2024)
摘要
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 ≉t
C with x ∉vars(t) by C{x ↦ 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 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要