Rewrite Techniques in

Theorem Proving Part III: Redundancy

Leo Bachmair Harald Ganzinger

CADE’94

Overview

We discuss superposition as a special case of subterm chaining with equality relations. Furthermore, we outline how saturated sets of formulas may be constructed and use the notion of fairness to establish a corresponding connection between dynamic and static aspects of the theorem proving process.

Superposition

We may use subterm chaining as the basic inference rule for dealing with equality.

(Positive) Superposition

\frac{C ∨ s ≈ t D ∨ u[s′] ≈ v}{(C ∨ D ∨ u[t] ≈ v)σ}

(Negative) Superposition

\frac{C ∨ s ≈ t D ∨ ¬( u[s′] ≈ v)}{(C ∨ D ∨ u[t] ≈ v)σ}

where (i) σ is a most general unifier of s and s′ and (ii) s′ is not a variable.

Example

Suppose a ≻ b ≻ c ≻ d and consider the following clauses:

c ≉ d

b ≈ d

a ≉ d ∨ a ≈ c

a ≈ b ∨ a ≈ d

By superposition we obtain

a ≉ d ∨ a ≈ d ∨ b ≈ c

If we disregard tautologies, no other clauses can be deduced by superposition, yet the given clause set is inconsistent.

Equality factoring

Transitivity resolution can be replaced by a considerably more restrictive inference rule that also subsumes factoring.

Equality Factoring

\frac{C ∨ u′ ≈ v′ ∨ u ≈ v}{(C ∨ v ≈ v′ ∨ u′ ≈ v′)σ}

where σ is a most general unifier of u and u′.

Example

Continuing with the example above, we see that there is also an equality factoring inference

\frac{a ≈ b ∨ a ≈ d}{b ≉ d ∨ a ≈ d}

We may use the conclusion of this inference for superposition, in

\frac{b ≉ d ∨ a ≈ d a ≉ d ∨ a ≈ c}{a ≉ d ∨ b ≉ d ∨ c ≈ d}

and again in

\frac{b ≉ d ∨ a ≈ d a ≉ d ∨ b ≉ d ∨ c ≈ d}{d ≉ d ∨ b ≉ d ∨ b ≉ d ∨ c ≈ d}

and eventually derive a contradiction.

Resolution and factoring

Positive factoring is essentially a special case of equality factoring. For example, we have

\frac{C ∨ s ≈ t ∨ s ≈ t}{C ∨ t ≉ t ∨ s ≈ t}

Similarly, resolution is a special case of superposition, if we encode non-equality atoms A as equations A ≈ ⊤. For example,

\frac{C ∨ A ≈ ⊤ D ∨ ¬(A ≈ ⊤)}{C ∨ D ∨ ⊤ ≉ ⊤}

Redundancy of Clauses

Let E be the set of all equality axioms (reflexivity, symmetry, transitivity, congruence). Recall that a ground clause C is Eredundant with respect to a set N if there exist ground instances C_{1}, …, C_{n} of N such that

C_{1}, …, C_{n}, E ⊧ C and
C ≻ C_{1}, …, C_{n}.

A clause is E-redundant in N if all its ground instances are.

Examples

The following clauses are all E-redundant:

C ∨ A ∨ ¬A (tautologies)
C ∨ t ≉ t
s ≉ v ∨ t ≉ v ∨ s ≈ t

Furthermore subsumed clauses are redundant. That is, a clause C ∨ D is redundant in the presence of C.

Redundancy of Inferences

A ground superposition inference

\frac{C D}{D′}

where D ≻ C is E-redundant with respect to N if either some premise is redundant or else there exist ground instances C_{1}, …, C_{n} of N such that

C_{1}, …, C_{n}, E ⊧ D′ and
D ≻ C_{1}, …, C_{n}.

An inference is E-redundant if all its ground instances are.

Superposition into variables

We have explicitly excluded superposition on variable subterms. This restriction is a consequence of our notion of redundancy. For example, if u ≻ v and f(u, u) ≻ g(u), then the superposition inference

\frac{u ≈ v f(x, x) ≈ g(x)}{f(u, v) ≈ g(u)}

is redundant. Any ground instance has as second premise an instance of f(u, u) ≈ g(u). But the latter formula logically follows from the smaller formulas u ≈ v and f(v, v) ≈ v and the equality axioms; and hence is redundant. Note that superposition from a (unshielded) variable is still required.

Saturation up to Redundancy

A set N is saturated up to redundancy if all inferences from N are redundant (with respect to N). Theorem.

Let N be a set of clauses that is saturated up to E-redundancy under superposition and equality factoring. Then N is unsatisfiable if and only if it contains the empty clause.

Remarks.

A superposition inference is redundant if its conclusion is already present. Equality factoring can be replaced by merging paramodulation.

Refutational theorem proving

Theorem provers typically consist of two components:

• A deductive inference system that is used to generate new formulas, and

• techniques for simplifying formulas and eliminating redundancies.

Example.

Inference system: Hyper-resolution Redundancy criteria: Tautology deletion and subsumption

Often a distinction is made between forward and backward simplification.

Theorem proving derivations

Let J be an inference system and R be a redundancy criterion. A theorem proving derivation is a sequence

N_{0} ⊢ N_{1} ⊢ N_{2} ⊢ ⋯

of sets of formulas, such that for all i N_{i+1} \ N_{i} ⊆ J (N_{i}) and

N_{i} \ N_{i+1} ⊆ R(N_{i+1}).

The limit of a derivation is the set

N_{∞} = ⋃_{i} ⋂_{j≥i} N_{j} of all persisting formulas.

Redundancy criteria

Let RF(N) and RJ (N) be the sets of formulas and inferences, respectively, that are deemed to be redundant in the context of a set N. We say that R = (RF, RJ) is a redundancy criterion if

1. if N ⊆ N′, then R(N) ⊆ R(N′)

2. if N′ ⊆ RF(N), then RJ (N) ⊆ RJ (N \ N′)

Fairness

A derivation is fair if every non-redundant inference from N_{∞} is redundant with respect to some set N_{j}, i.e.

J (N_{∞}) \ RJ (N_{∞}) ⊆ ⋃_{j} RJ (N_{j}).

Theorem.

The limit of a fair derivation is saturated up to redundancy

We say that J is compatible with R if an inference is redundant whenever its conclusion is already present. Proposition.

If J is compatible with R, then a derivation is fair if the conclusion of every non-redundant inference from N_{∞} is contained in some set N_{k}.

Simplification

Simplification is the combination of deduction and deletion. Example.

Let N be N_{0} ∪ {A ∨ B, A ∨ ¬B ∨ C}. Then

N ⊢ N ∪ {A ∨ C}

by resolution plus factoring. Also,

N ∪ {A ∨ C} ⊢ N_{0} ∪ {A ∨ B, A ∨ C}

by subsumption. These two steps are often combined into resolution with subsumption:

N ⊢ N_{0} ∪ {A ∨ B, A ∨ C}.

Simplification by rewriting

Suppose the set N contains equations

−x ∗ y + y ∗ x ≈ y ∗ 0 and
z ∗ 0 ≈ 0

We may deduce

−x ∗ y + y ∗ x ≈ 0

(by paramodulation, not superposition) and then delete

−x ∗ y + y ∗ x ≈ y ∗ 0

The combination of these derivation steps is known as simplification by rewriting or demodulation.

Fundamental theorem proving concepts and techniques

Deduction Redundancy (simplification) Constraints

Selection Orderings Extension by definition Polarity

Commutation Chaining Basic strategy

Literature

L. Bachmair and H. Ganzinger, Rewritebased equational theorem proving with selection and simplification. Journal of Logic and Computation 4 (1994):217–247.

• describes superposition with selection

• proposes two notions of redundancy

• describes simplification techniques

• refutations in saturated theories