Rewrite Techniques in Theorem Proving Part II: Chaining

Leo Bachmair Harald Ganzinger

Tutorial—CADE’94

Contents

Efficient handling of transitivity

x ≮ y , y ≮ z , x < z  (T )

through rewrite techniques.

Applications • equality, partial congruences

• orderings

• consequence relations, modal logics, higher-order logic, set theory

• non-deterministic computations

Chaining

Hyperresolution with transitivity

\frac{C , u < v D , s < t x ≮ y , y ≮ z , x < z}{(C , D , u < t)σ}

where σ = mgu(v, s).

Chaining [Slagle 72]:

\frac{C, u < v D, s < t}{(C, D, u < t)σ}  σ = mgu(v, s)

Theorem 1 Ordered resolution (not involving T ) + chaining is complete.

Proof. Ordered resolution with selection is complete: select both negative literals of T . □

Problems

• the transitive closure of < is naively and completely enumerated: Ω(n^{3}) in the finite case

• infinite transitive closures

• s < t chains in both directions from s to t and from t to s

• chaining through variables: x < s(x) and p(y) < y generate p^{m}(x) < s^{n}(x), for all n, m

• handling of additional properties such as monotonicity

x < y → f(…, x, …) < f(…, y …)

or anti-symmetry

x ≤ y , y ≤ x → x ≈ y

Infinitary Depth-First Search

Let G = (V, E) be a possibly infinite graph.

Depth-first search of G

• define some well-founded, total ordering ≻ on V

• search G_{1} = (V, E ∩ ⪰) and G_{2} = (V, E^{−1} ∩ ⪰)

• combine the results

Here:

• V = set of ground terms

• E = set of inequations s < t

• ≻ = some complete reduction ordering

Syntactic Orderings ≻

Given a < b < c < d < e < f < g < h define syntactic ordering a ≻ d ≻ f ≻ e ≻ h ≻ g ≻ b ≻ c

[figure: ≻; <; a; b; c; d; e; f; g; h]

two rewrite relations

.<. = < ∩ ⪰ and .<. = < ∩ ⪯

Making Peaks Commute

… by adding chains through peaks.

[figure: ≻; <; a; b; c; d; e; f; g; h]

Result. x <^{+} y iff x = x_{0} .<. . . . .<. x_{n} = y_{k} .<. . . . .<. y_{0} = y, where n + k ≥ 1. This is a rewrite proof of x <^{+} y.

Commutation

Let R ⊕ S = (R^{∗} ∘ S^{+}) ∪ (R^{+} ∘ S^{∗}).

Definition .<. commutes over .<. iff

[figure: .<. ∘ .<. ⊆ .<. ⊕ .<..; ⊕]

Proposition

[figure: ⊕; iff; ⊕; ⊕; .; .; .; ⊕]

Hence: Commutation is equivalent with the existence of rewrite proofs for <^{+}. If .<. = .<.^{−1} we speak of the local confluence of .<. (and .<.).

Ordered Chaining

One achieves commutation by computing all chaining inferences through peaks.

From now on let ≻ be a complete reduction ordering on terms, and let ≻ also denote its lexicographic extension to inequations.

Ordered Chaining (Unit Case) B_{<}

\frac{u < s t < v}{uσ < vσ}

where σ = mgu(s, t), uσ ⪰̸ sσ, and vσ ⪰̸ sσ.

Redundancy of Clauses

A ground clause C is called T -redundant in a set N of clauses iff

1. C_{1}, …, C_{n}, T ⊧ C

2. C ≻ C_{i}, where the C_{i} are ground instances of N. A clause is T -redundant in N if all its ground instances are.

Redundancy of Inferences

An inference from ground clauses

\frac{D_{1}, …, D_{n}}{C}

is called T -redundant in N if one of the D_{i} is T -redundant in N, or else if

1. C_{1}, …, C_{n}, T ⊧ C

2. D ≻ C_{i}, with D = max_{≻}D_{i}, where the C_{i} are ground instances of N. An inference is T -redundant in N if all its ground instances are.

Saturation up to Redundancy

Let I be an inference system.

N is saturated (with respect to I) up to redundancy if all inferences from N in I are T -redundant in N.

Note:

• If an inference is monotone, i.e., D ≻ C, it becomes redundant when we add its conclusion to N.

• All inference systems that we consider are monotone.

• For more on how to saturate a set of clauses see part III.

• The given notion of redundancy is not compatible with arbitrary inference systems. In particular, inference systems for clauses with constraints come with a modified notion of redundancy.

Model Construction

Given a set of ground inequations and an ordering ≻, define, for each inequation C = s < t, Herbrand interpretations I_{C} and I^{C} and an auxiliary set E_{C} as follows:

I_{C} = ( ⋃_{C≻D} E_{D})^{∨}

E_{C} = \{ \begin{matrix}\{s < t\}, & if s < t not in I_{C} \\ ∅, & otherwise \end{matrix}
I^{C} = (I_{C} ∪ E_{C})^{∨}

where R^{∨} is the rewrite closure of R. Finally I = (⋃_{C} E_{C})^{∨}.

C is called productive if E_{C} ≠ ∅. R_{C} = ⋃_{C≻D} E_{D}

Main Lemma

Lemma 1 Let N be a set of ground inequations that is saturated under B_{<} up to T -redundancy. Then for every inequation C in N we have:

1. If C is T -redundant in N then C is in I_{C}.

2. If C is a productive inequation it is not T -redundant in N.

3. I_{C} and I^{C} are transitive, i.e. satisfy T .

4. C is in I^{C}.

Proof of the Lemma

By induction over ≻.

(1) If C is redundant, then C_{1}, …, C_{n}, T ⊧ C, for inequations C_{i} in N such that C ≻ C_{i}. By induction hypothesis for (4), C_{i} is in I_{C} and, by induction hypothesis for (3), T is true in I_{C}. Hence C is in I_{C}.

(2) If C is productive then C is not in I_{C}. By (1) it is therefore not redundant.

(3) By induction hypothesis, all peaks involving inequations in R_{C} commute. The cases E_{C} = ∅ or s = t are trivial. Otherwise and if C = s .<. t R_{C} cannot contain any inequation t .<. u as inequations of this form are bigger than C. In the remaining case E_{C} = {s .<. t}. Suppose there is an inequation C′ = u .<. s in R_{C}. As N is saturated, the inference from C′ and C by ordered chaining produces u < t and is redundant in N. Being productive, by (2) neither C nor C′ can be redundant, hence u < t must follow from T and from clauses C_{i} in N which are smaller than C. Applying the induction hypothesis for (4) we conclude that u < t is in I_{C}.

(4) C ∈ I_{C} ∪ E_{C} by construction.

Completeness

Theorem 2 Let N be a set of inequations and saturated under B_{<} up to T -redundancy. Let s and t be ground terms. Then s < t follows from N ∪ {T } iff s < t has a rewrite proof in ground instances of N.

Proof. We apply the lemma to the ground instances of N. By standard lifting arguments it follows that if N is saturated so is the set of its ground instances. Let I be the interpretation constructed from the latter. Then: s < t follows from N ∪ {T }

⇒ s < t true in I [lemma: (3), (4)] ⇒ s < t has rewrite proof consisting of (productive) instances of N.

□

Applications

• testing N ∪ {T } ⊧ s < t by rewriting

• solving inequations s < t over N ∪ {T } by narrowing-like procedures: negative chaining

• extension of the calculus to Horn clauses

Calculus B_{<} for Horn Clauses

Ordered Chaining

\frac{C → u .<. s D → t .<. v}{\{C , D → u < v\}σ}

where

(i) σ = mgu(s, t), (ii) Cσ ⪰̸ (u < s)σ, (iii) Dσ ⪰̸ (t < v)σ, (iv) uσ ⪰̸ sσ, and

(v) vσ ⪰̸ sσ. In what follows we specify maximality constraints for literals in clauses by boxes, and those for terms in literals by using .<. and .<. as indicated above.

Horn Clauses II

Negative chaining

\frac{Γ , u .<. s → Δ Λ → t .<. v}{\{Γ , Λ , v < s → Δ\}σ}

where σ = mgu(u, t); and

\frac{Γ , u .<. s → Δ Λ → t .<. v}{\{Γ , Λ , u < t → Δ\}σ}

where σ = mgu(s, v). Ordered resolution

\frac{Γ , A ¬B , Λ}{Γσ , Λσ}

where σ = mgu(A, B).

Completeness of B_{<}

Theorem 3 Let N be a set of Horn clauses and saturated under B_{<} up to T -redundancy. Then N is satisfiable iff the empty clause is not in N.

Proof. We combine the criteria for productivity for general clauses (cf. part I) with those for inequations as follows:

E_{C} = \{ \begin{matrix}\{s < t\}, & if (i) – (iii) \\ ∅, & otherwise \end{matrix}

where

(i) C is false in I_{C},

(ii) C is of the form Γ → s < t, (iii) (s < t) ≻ Γ,

and, as before,

I_{C} = ( ⋃ ; C≻D ED)^{∨}.

□

Variable Chaining

Proposition 1 Chaining through shielded variables is not needed.

Proposition 2 Chaining into non-linear, unshielded variables is required.

Proof. Consider this unsatisfiable set

→ a .<. a′
→ a′ .<. c
→ b .<. b′
→ b′ .<. c
a < x, b < x →

where c ≻ b′ ≻ b ≻ a′ ≻ a. Without chaining into variables, B_{<} only produces a .<. b′ → and a .<. b →. □

Calculus C_{<} for Clauses

C_{<} is B_{<} together with:

Ordered factoring

\frac{Γ , A , B}{Γσ , Aσ}

where σ = mgu(A, B)

Transitivity resolution

\frac{C , u .<. v , u′ .<. v′ D , s .<. t}{\{D , t ≮ v′ , s < v′\}σ}

where σ = mgu(u, u′, s).

TR specializes further in the presence of additional logical properties.

Theorem 4 Let N be a set of clauses and saturated under C_{<} up to T -redundancy. Then N is satisfiable iff the empty clause is not in N.

Monotonicity

Subterm Chaining

\frac{C , u .<. s D , w[t] .<. v}{\{C , D , w[u] < v\}σ}

where • σ = mgu(s, t),

• t a subterm of w, including subterms at or below variables,

• the functions above t in w are mono-

tonic wrt. <. Similarly for anti-monotonicity.

Composition of Relations

Composition laws of the form

x ⊕ y , y ⊖ z → x ⊗ z

can be translated into Ordered composition

\frac{u ⊕ s t ⊖ v}{uσ ⊗ vσ}

where σ = mgu(s, t), uσ ⪰̸ sσ, and vσ ⪰̸ sσ. Examples

x < y , y < z → x < z
x ≤ y , y < z → x < z
x ≈ y , y ⊕ z → x ⊕ z
x ∈ y , y ⊆ z → x ∈ z

Summary

• commutation yields rewrite proofs for transitive relations

• similarly for almost arbitrary composition laws

• chaining required for peaks only ⇒ ordered inferences

• monotonicity properties require chaining through subterms

• straightforward extension to Horn clauses; disjunctions somewhat more involved

• abstract notion of redundancy

• inference systems compatible with redundancy

• problem of chaining at or below variables: ok for symmetric relations (cf. part III) and for dense total orderings (cf. CADE conference)

Literature I

L. Bachmair, H. Ganzinger, 1993. Rewrite Techniques for Transitive Relations. TR MPI-I-93-249, MPI Informatik, Saarbrücken. Short version in Proc. LICS’94.

• describes system C_{<} with completeness proof

• discusses influence of symmetry and monotonicity

L. Bachmair, H. Ganzinger, 1993. Ordered Chaining for Total Orderings. TR MPI-I-93-250, MPI Informatik, Saarbrücken. Short version in Proc. CADE’94.

• describes maximal chaining for total orderings, together with completeness proof

• chaining for equality and inequality

• variable elimination as simplification

• reports experimental results (Saturate system)

Literature II

J. Levy, J. Agustí, 1993. Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations. In C. Kirchner, editor, Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 690, pp. 17–31.

• bi-rewriting = 2 commuting rewrite systems

• considers unit inequations and monotonic transitive relations

• application to lattice theory with discussion of variable chaining

P. Nivela, R. Nieuwenhuis, H. Ganzinger, 1994. Overview of the Saturate System. Hypertext document on the world-wide web at

“ftp://ftp.mpi-sb.mpg.de/pub/SATURATE/Saturate.html”.

• describes the usage of the Saturate system, featuring

– orderd chaining (with selection) for arbitrary composition laws

– constraint solving for lpo constraints

– simplification techniques, including tautology deletion by ground chaining, subsumption, reduction, case analysis, clausal rewriting

• applications of Saturate to problems in equational logic, modal logic, verification of quicksort