2024/05/06 by Uwe Waldmann, Waldmann, Uwe
Computer Science · #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Matrix Theory and Algorithms
paper · pdf · doi:10.48550/arxiv.2405.03367
openalex publication_date 2024/05/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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≈ 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.