On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus

TL;DR

This paper investigates the impact of Destructive Equality Resolution on the completeness of the Superposition Calculus, showing that naive inclusion causes incompleteness, but certain restricted variants remain complete.

Contribution

It identifies the incompleteness issue caused by Destructive Equality Resolution and proposes restricted calculus variants that preserve refutational completeness.

Findings

Naive addition of Destructive Equality Resolution leads to incompleteness.

Restricted variants of the calculus maintain completeness with Destructive Equality Resolution.

The study clarifies the conditions under which Destructive Equality Resolution can be safely used.

Abstract

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.