Rewrite Techniques in Theorem Proving Part I: Orderings

Leo Bachmair Harald Ganzinger

CADE’94

Overview

We will show how (well-founded) orderings can be used to

• refine inference rules

• construct distinguished models for certain clause sets

• prove the refutational completeness of inference systems

Clauses

A clause is a finite multiset of literals, written either as a disjunction

¬A_{1} ∨ ⋯ ∨ ¬A_{m} ∨ B_{1} ∨ ⋯ ∨ B_{n} or as a sequent

A_{1}, …, A_{m} → B_{1}, …, B_{n}

Herbrand interpretations

An (Herbrand) interpretation is a set I of ground (variable-free) atomic formulas.

If A ∈ I, then A is true (and ¬A

false) in I; if A ∉ I, then A is false (and ¬A

true) in I.

A ground clause is true if at least one of its literals is true. A non-ground clause is true if all its ground instances are true.

Refutational theorem proving

A set of clauses is satisfiable if there exists an interpretation in which all its clauses are true; and unsatisfiable otherwise.

Refutational theorem provers attempt to determine whether a formula

F logically follows from a set N

by checking whether the set of clauses corresponding to

N ∪ {¬F } is unsatisfiable.

Well-founded orderings

An ordering ≻ is said to be wellfounded if there is no infinite sequence

x_{1} ≻ x_{2} ≻ x_{3} ≻ ⋯

An ordering ≻ can be extended to multisets as follows:

M ≻ N if and only if

M ≠ N and, whenever M(x) < N(x), then N(y) < M(y), for some y with y ≻ x.

Example.

{5} ≻ {1, 1, 2, 4, 4, 4}

Example

Consider the following clauses (listed in increasing order by size):

P (0) P (0) ∨ P (s0) P (s0) ∨ P (ss0) … P (s^{2n−1}0) ∨ P (s^{2n}0) P (s^{2n}0) ∨ P (s^{2n+1}0) …

Example (cont.)

We use the wellfounded ordering to construct a model.

Clause set  Interpretation
P (0)  P (0)

P (0) ∨ P (s0)

P (s0) ∨ P (ss0)  P (ss0)
…  …
P (s^{2n−1}0) ∨ P (s^{2n}0)  P (s^{2n}0)

P (s^{2n}0) ∨ P (s^{2n+1}0)

…  …

Model construction

Given a set of ground clauses and a total wellfounded ordering ≻, define for each clause C a Herbrand interpretation I_{C} and an auxiliary set E_{C}. More specifically,

I_{C} = ⋃_{C≻D} E_{D}

and

E_{C} = \{A\} if \{ \begin{matrix}(i) C is false in I_{C} \\ (ii) C = Γ → Δ, A \\ (iii) A ≻ Γ, Δ \end{matrix}

E_{C} = ∅ otherwise.

If E_{C} ≠ ∅ the clause C is called productive. Finally,

I = ⋃_{C} E_{C}

Model construction (cont.)

Productive clauses are evidently true in I, but non-productive clauses may be false. Example. Suppose ¬B ≻ B ≻ A and consider the clauses

A →
→ A, B
B →

The second clause is the only productive clause; it produces B. Hence

I = {B}

and the third clause is false.

Minimal counter-examples

A minimal counter-example is a smallest clause false in I (e.g. the third clause in the example above).

Note.

A minimal counter-example is nonproductive; hence must violate one of the conditions imposed on productive clauses. We shall distinguish two cases, depending on whether the second or the third condition is violated.

Ground resolution

Taking the above example, we see that

B →

is the minimal counter-example and

→ A, B

produces B. Look at the resolution inference

\frac{→ A, B B →}{→ A}

The conclusion is a smaller counterexample!

Thus, if a set of clauses is closed under resolution, there are no minimal counterexamples of this kind.

Positive factoring

Take the clauses

A →
→ A, B, B
B →

There is no productive clause; the second clause is the minimal counter-example. The factoring inference

\frac{→ A, B, B}{→ A, B}

yields a smaller counter-example. Thus, if a set of clauses is closed under positive factoring, this kind of counterexample cannot be present.

Selection

Let ≻ be a well-founded ordering and S be a (partial) function that selects negative literals in clauses. Ordered Ground Resolution

\frac{Γ → Δ, A A, Σ → Π}{Γ, Σ → Δ, Π}

if (i) A is maximal in the first premise and selected or maximal in the second premise and (ii) the first premise contains no selected literals.

Positive Ground Factoring

\frac{Γ → Δ, A, A}{Γ → Δ, A}

if (i) A is maximal in the premise and (ii) the premise contains no selected literals.

Refutational Completeness

Theorem.

If a set of (ground) clauses is saturated under ordered resolution with selection and under positive factoring, then it is unsatisfiable if and only if it contains the empty clause.

Remarks

1. Productive clauses are conditional rewrite rules with positive and negative conditions. They define a perfect model in the logic programming sense.

2. Hyperresolution can be simulated by ordered resolution with selection.

3. Tautologies and subsumed clauses can neither be minimal counter-examples nor productive. They are redundant!

Lock resolution

Example.

\begin{matrix}A_{1} & ∨ & B_{5} \\ ¬A_{2} & ∨ & ¬B_{6} \\ A_{7} & ∨ & ¬B_{3} \\ ¬A_{8} & ∨ & B_{4} \end{matrix}

Resolve only on literals with minimal index:

\begin{matrix}B_{5} & ∨ & ¬B_{6} \\ A_{7} & ∨ & ¬A_{8} \end{matrix}

If we delete tautologies, no contradiction can be deduced!

Lock resolution as ordered resolution

First introduce new literals:

\begin{matrix}L_{1,1} ⊃ A & L_{1,2} ⊃ B \\ L_{2,1} ⊃ ¬A & L_{2,2} ⊃ ¬B \\ L_{3,1} ⊃ A & L_{3,2} ⊃ ¬B \\ L_{4,1} ⊃ ¬A & L_{4,2} ⊃ B \end{matrix}

Then saturate under ordered resolution with A, B ≻ L_{i,j}, e.g.

\frac{¬L_{1,1} ∨ A L_{2,1} ∨ ¬A}{¬L_{1,1} ∨ ¬L_{2,1}}

The result is a set of connections:

¬L_{1,1} ∨ ¬L_{2,1}

¬L_{1,1} ∨ ¬L_{4,1}
…
¬L_{3,2} ∨ ¬L_{4,2}

Lock resolution as ordered resolution (cont.)

Then encode original clauses:

L_{1,1} ∨ L_{1,2} L_{2,1} ∨ L_{2,2} L_{3,1} ∨ L_{3,2} L_{4,1} ∨ L_{4,2}

Finally apply (negative) ordered hyperresolution with an ordering that reflects the indexing in the original clauses, e.g.

\frac{L_{1,1} ∨ L_{1,2} L_{2,1} ∨ L_{2,2} ¬L_{1,1} ∨ ¬L_{2,1}}{L_{1,2} ∨ L_{2,2}}

Note.

The inverse method can be encoded in a similar fashion.

Literature

Further details can be found in:

L. Bachmair and H. Ganzinger. Nonclausal resolution and superposition with selection and redundancy criteria. Proc. LPAR 92, LNAI 624. Springer-Verlag, 1992, pp. 273–284.

L. Bachmair and H. Ganzinger. Perfect model semantics for logic programs with equality, Proc. ICLP 91. MIT Press, 1991, pp. 645–659.