The Saturation Procedure

The basic CNF saturation procedure is :

While a refutation has not been found
    Copy two clauses from the set
    Generate all logical consequences, e.g., by resolution
    Put logical consequences into the set

Note the "Copy", indicating that a clause may be used multiple times with a new set of variables each time.

Example

S = { wise(jim), ~wise(X) | wise(brother_of(X)), ~wise(brother_of(brother_of(jim))) }

~wise(X) | wise(brother_of(X)) + ~wise(brother_of(brother_of(jim)))

» ~wise(brother_of(jim))

~wise(brother_of(jim)) + ~wise(X) | wise(brother_of(X))

» ~wise(jim)

wise(jim) + ~wise(jim)

» FALSE

Example

S = { p(f(X)) | q(Y), ~p(X) | q(dog), p(f(dog)) | ~q(X), ~p(f(Z)) }

p(f(X)) | q(Y) + ~p(X) | q(dog) » q(dog) | q(Y)

p(f(dog)) | ~q(X) + ~p(f(Z)) » ~q(X)

q(dog) | q(Y) + ~q(X) » FALSE

Example

A = { ∀X(p(X) => ∃Y(~q(X) => r(Y)), ~p(a) => p(b), ∀Y ~q(Y) } C = ∃X r(X)

Example
A = { ∀X(p(X) => ∃Y(~q(X) => r(Y)), ~p(a) => p(b), ∀Y ~q(Y) } C = ∃X r(X)

Full resolution is refutation complete for general clauses [Robinson 1965], and binary resolution is refutation complete for Horn clauses [Henschen & Wos 1974]. This means that if the input set is unsatisfiable, then the empty clause can always be derived in this manner, given infinite time and memory (i.e., resolution is theoretically refutation complete, practically incomplete). Such a deduction is called a refutation. If the input set is satisfiable, the resolution procedure may continue for ever.

Proof Trees

A refutation can be represented as a proof tree.

Example

S2 = { ~p(X) | q(X) | r(X), p(a) | p(b), ~q(Y), ~r(a), ~r(b) }

~p(X) | q(X) | r(X) + ~q(Y) » ~p(X) | r(X)

~p(X) | r(X) + ~r(a) » ~p(a)

+ ~r(b) » ~p(b)

~p(a) + p(a) | p(b) » p(b)

p(b) + ~p(b) » FALSE

This refutation has the proof tree :

Notice that the clause ~p(X) | r(X) is used twice in the proof tree but is generated only once by resolution.

Failure Trees

A failure tree for an unsatisfiable set of clauses is a minimal finite sub-tree of a fair semantic tree for the Herbrand base, such that for each branch there is a clause that is FALSE in the sub-interpretation identified by that branch. FALSE has a single node as its failure tree.

Example

S = { wise(jim), ~wise(X) | wise(brother_of(X)), ~wise(brother_of(brother_of(jim))) }

Example
S = { wise(jim), ~wise(X) \| wise(brother_of(X)), ~wise(brother_of(brother_of(jim))) }

This unsatisfiable clause set has the failure tree :

Example

S = { p(a) | q(X), ~p(Y) | q(f(Y)), p(a) | ~q(T), ~p(a) | ~q(W) }

Example
S = { p(a) \| q(X), ~p(Y) \| q(f(Y)), p(a) \| ~q(T), ~p(a) \| ~q(W) }

A Herbrand unsatisfiable set of clauses has a failure tree

Proof

If a set of clauses is Herbrand unsatisfiable then for each branch of a fair semantic tree of the Herbrand base, i.e., for each Herbrand interpretation, there exists a clause in the set that has a ground instance that is FALSE in the Herbrand interpretation identified by that branch. As there are only a finite number of literals in each clause, and each literal has finite depth, each such branch has a shortest sub-branch such that the FALSE interpretation of the clause (instance) is determined by the sub-interpretation identified by the sub-branch. The leaf of such a sub-branch is a failure node for the clause. The sub-branches define a finite sub-tree of the semantic tree. Prune any descendants of failure nodes to form a minimal finite sub-tree, i.e. a failure tree.

Proof
If a set of clauses is Herbrand unsatisfiable then for each branch of a fair semantic tree of the Herbrand base, i.e., for each Herbrand interpretation, there exists a clause in the set that has a ground instance that is FALSE in the Herbrand interpretation identified by that branch. As there are only a finite number of literals in each clause, and each literal has finite depth, each such branch has a shortest sub-branch such that the FALSE interpretation of the clause (instance) is determined by the sub-interpretation identified by the sub-branch. The leaf of such a sub-branch is a failure node for the clause. The sub-branches define a finite sub-tree of the semantic tree. Prune any descendants of failure nodes to form a minimal finite sub-tree, i.e. a failure tree.

Failures trees are used in the proof of the completeness of resolution.

Refutation Completeness

The CNF saturation procedure with resolution is refutation complete

Proof

For a set of clauses S, let R(S) mean S ∪ {all resolvants from S}, and Rⁿ(S) mean R applied n times. If S is Herbrand unsatisfiable, then it needs to be shown that there exists n such that FALSE is an element of Rⁿ(S).
If S is unsatisfiable, then it has a failure tree. If the tree is trivial, then FALSE is an element of S. Otherwise:

Pick a failure node Y of maximum depth in the failure tree. Let X be the parent of Y. X is not a failure node as a failure tree is minimal. Let Z be the other offspring, which must also be a failure node as Y is of maximum depth.
Let K be the Herbrand base element whose truth value is determined by the arcs X-Y (FALSE) and X-Z (TRUE).
As Y and Z are failure nodes, there exist clauses that are FALSE at Y and Z respectively. Since both these clauses are not FALSE at X (X is not a failure node) the clauses must be of the forms C^| | L₁ |...| L_n and D^| | ~M₁ |...| ~M_n, such that they have ground instances (C^| | L₁ |...| L_n)θ and (D^| | ~M₁ |...| ~M_n)σ, and L_iθ = M_jσ = K.
Then there is a resolvant (C^| | D^|)γ of the clauses. (C^| | D^|)θσ is an instance of (C^| | D^|)γ. All literals of (C^| | D^|)θσ are FALSE at some highest node F above Y and Z. This node is a failure node for (C^| | D^|)γ. The failure tree for S ∪ {(C^| | D^|)γ} is thus smaller than that for S.
If S is unsatisfiable, then S ∪ {(C^| | D^|)γ} is unsatisfiable (simply because S is unsatisfiable), so the process can be iterated. As the failure tree keeps getting smaller, it must eventually become the trivial tree. FALSE has then been inferred.

Note that the failure tree has a maximal depth equal to the size of the Herbrand Base, i.e., infinite. Thus the number of resolutions that might be necessary is the same.
Example
The failure tree for:
S = { wise(jim), ~wise(X) | wise(brother_of(X)), ~wise(brother_of(brother_of(jim))) }
is

X, Y and Z are as indicated. K = wise(brother_of(brother_of(jim)))
The clause that is FALSE at Y is ~wise(X) | wise(brother_of(X)), and the clause that is FALSE at Z is ~wise(brother_of(brother_of(jim)))
With θ = {X/brother_of(jim)} and σ = {}, the ground instances of these clauses are ~wise(brother_of(jim)) | wise(brother_of(brother_of(jim))) and ~wise(brother_of(brother_of(jim))).
With γ = {X/brother_of(jim)} the resolvant of these clauses is ~wise(brother_of(jim)), which is FALSE at the node F.
The failure tree for
S = { wise(jim), ~wise(X) | wise(brother_of(X)), ~wise(brother_of(brother_of(jim))), ~wise(brother_of(jim)) }
is

Proof
For a set of clauses S, let R(S) mean S ∪ {all resolvants from S}, and Rⁿ(S) mean R applied n times. If S is Herbrand unsatisfiable, then it needs to be shown that there exists n such that `FALSE` is an element of Rⁿ(S). If S is unsatisfiable, then it has a failure tree. If the tree is trivial, then `FALSE` is an element of S. Otherwise: Pick a failure node Y of maximum depth in the failure tree. Let X be the parent of Y. X is not a failure node as a failure tree is minimal. Let Z be the other offspring, which must also be a failure node as Y is of maximum depth. Let `K` be the Herbrand base element whose truth value is determined by the arcs X-Y (`FALSE`) and X-Z (`TRUE`). As Y and Z are failure nodes, there exist clauses that are `FALSE` at Y and Z respectively. Since both these clauses are not `FALSE` at X (X is not a failure node) the clauses must be of the forms `C^\| \| L₁ \|...\| L_n` and `D^\| \| ~M₁ \|...\| ~M_n`, such that they have ground instances `(C^\| \| L₁ \|...\| L_n)θ` and `(D^\| \| ~M₁ \|...\| ~M_n)σ`, and `L_iθ = M_jσ = K`. Then there is a resolvant `(C^\| \| D^\|)γ` of the clauses. `(C^\| \| D^\|)θσ` is an instance of `(C^\| \| D^\|)γ`. All literals of `(C^\| \| D^\|)θσ` are `FALSE` at some highest node F above Y and Z. This node is a failure node for `(C^\| \| D^\|)γ`. The failure tree for S ∪ `{(C^\| \| D^\|)γ}` is thus smaller than that for S. If S is unsatisfiable, then S ∪ `{(C^\| \| D^\|)γ}` is unsatisfiable (simply because S is unsatisfiable), so the process can be iterated. As the failure tree keeps getting smaller, it must eventually become the trivial tree. `FALSE` has then been inferred. Note that the failure tree has a maximal depth equal to the size of the Herbrand Base, i.e., infinite. Thus the number of resolutions that might be necessary is the same.
Example
The failure tree for: S = { wise(jim), ~wise(X) \| wise(brother_of(X)), ~wise(brother_of(brother_of(jim))) } is X, Y and Z are as indicated. K = `wise(brother_of(brother_of(jim)))` The clause that is `FALSE` at Y is `~wise(X) \| wise(brother_of(X))`, and the clause that is `FALSE` at Z is `~wise(brother_of(brother_of(jim)))` With `θ = {X/brother_of(jim)}` and `σ = {}`, the ground instances of these clauses are `~wise(brother_of(jim)) \| wise(brother_of(brother_of(jim)))` and `~wise(brother_of(brother_of(jim)))`. With `γ = {X/brother_of(jim)}` the resolvant of these clauses is `~wise(brother_of(jim))`, which is FALSE at the node F. The failure tree for S = { wise(jim), ~wise(X) \| wise(brother_of(X)), ~wise(brother_of(brother_of(jim))), ~wise(brother_of(jim)) } is

The Quest for Logical Consequence

To show that C is a logical consequence of Ax, it is necessary to:

Show that every model of Ax is a model of C
OR
Show that Ax ∪ {~C} is unsatisfiable.

Ax ∪ {~C} is unsatisfiable iff CNF(Ax ∪ {~C}) is unsatisfiable, so ...

Show that CNF(Ax ∪ {~C}) is unsatisfiable.

A set of clauses has a model iff it has a Herbrand model, so ...

Show that CNF(Ax ∪ {~C}) is Herbrand unsatisfiable.

An inference rule for clauses is sound if every Herbrand model of the parents is a Herbrand model of the inferred clauses, and resolution is a sound inference rule for clauses, so ...

Confidently use the basic clausal saturation procedure to find a refutation:

Form the set Ax ∪ {~C}
Convert the set to CNF(Ax ∪ {~C})
While a refutation has not been found
    Copy two clauses from the set
    Use resolution to generate logical consequences of the clauses
    Put the logical consequences into the set

Exam Style Questions

Write out the basic resolution procedure algorithm.
What things could happen if the basic resolution procedure algorithm is run on an unsatisfiable set of clauses?
What things could happen if the basic resolution procedure algorithm is run on a satisfiable set of clauses?
In what circumstances does the basic resolution procedure algorithm retain refutation completeness when using only binary resolution?

Draw the proof tree for the following refutation:

`~p(X) \| q(X) \| r(X)`	`+`	`~q(Y)`	»	`~p(X) \| r(X)`
`~p(X) \| r(X)`	`+`	`~r(a)`	»	`~p(a)`
	`+`	`~r(b)`	»	`~p(b)`
`~p(a)`	`+`	`p(a) \| p(b)`	»	`p(b)`
`p(b)`	`+`	`~p(b)`	»	`FALSE`

What is an axiomatic proof?

Draw the failure tree for the following set of clauses:

     S = { p(f(X)) | q(Y),
           ~p(X) | q(dog),
           p(f(dog)) | ~q(X),
           ~p(f(Z)) }

Prove that a Herbrand unsatisfiable set of clauses has a failure tree.
Prove that the resolution procedure is refutation complete.