Completeness and Limitations of Destructive Equality Resolution in the Superposition Calculus

Core Concepts

The naive addition of Destructive Equality Resolution (DER) to the standard abstract redundancy concept renders the Superposition Calculus refutationally incomplete, but several restricted variants of the calculus are refutationally complete even with DER.

Abstract

The paper investigates the impact of Destructive Equality Resolution (DER) on the refutational completeness of the Superposition Calculus. DER is a simplification technique that replaces a clause x ≠ t ∨ C with x ∉ vars(t) by C{x ↦ t}.
The key findings are:

The naive addition of DER to the standard abstract redundancy concept renders the calculus refutationally incomplete. An example is provided to demonstrate this.

Several restricted variants of the Superposition Calculus that are refutationally complete even with DER are presented. These include:

The ground closure Horn Superposition Calculus, which uses a specialized ordering ≻≻R to compare ground closures. This ordering takes into account the R-normalization of terms in the closures.

The inductive construction of a candidate interpretation R* by inspecting all ground closures containing the maximal term s simultaneously. If a closure satisfies the usual conditions for productivity, the ≻≻Rs-smallest such closure is used to extend Rs.
The paper shows that these restricted calculi maintain refutational completeness even with the addition of DER as a simplification rule.

Stats

None

Quotes

None

Key Insights Distilled From

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

by Uwe Waldmann at arxiv.org 05-07-2024

https://arxiv.org/pdf/2405.03367.pdf

Deeper Inquiries

How could the ideas presented in this paper be extended to handle non-Horn clauses

The ideas presented in the paper could be extended to handle non-Horn clauses by adapting the redundancy criterion and completeness proof to accommodate the complexities introduced by non-Horn clauses. This would involve considering a broader range of clause structures, such as clauses with multiple positive literals or clauses with more complex patterns of literals. The ordering ≻≻R could be modified to account for the additional intricacies of non-Horn clauses, ensuring that the completeness proof remains valid for this extended set of clauses. Additionally, the candidate interpretation construction process would need to be adjusted to handle the unique characteristics of non-Horn clauses, potentially requiring more sophisticated techniques for identifying productive closures and generating the candidate interpretation.

What are the practical implications of the incompleteness result for state-of-the-art superposition theorem provers that implement DER

The incompleteness result for state-of-the-art superposition theorem provers that implement Destructive Equality Resolution (DER) has significant practical implications. It indicates that the addition of DER as a simplification rule can lead to refutational incompleteness in the superposition calculus, potentially resulting in the saturation of an inconsistent set of clauses without deriving the empty clause. This means that theorem provers relying on DER for simplification may not be able to prove the unsatisfiability of certain sets of clauses, impacting their effectiveness in solving complex problems. As a result, developers and users of superposition provers need to be aware of this limitation and consider alternative strategies or modifications to ensure refutational completeness in their theorem proving processes.

Could the specialized ordering ≻≻R be generalized to handle non-ground clauses, and if so, how would that affect the completeness proof

The specialized ordering ≻≻R used in the paper could potentially be generalized to handle non-ground clauses by extending the concept of normalization closure ordering to non-ground terms and clauses. This generalization would involve adapting the ordering criteria to account for variables and substitutions in addition to ground terms, ensuring that the ordering remains well-defined and total on non-ground structures. By incorporating variables and substitutions into the ordering process, the completeness proof could be extended to cover a wider range of clause types, including non-ground clauses. This generalization would enhance the applicability of the ordering ≻≻R to a broader set of theorem proving scenarios, providing a more comprehensive framework for ensuring refutational completeness in superposition calculi.