The Resolution Inference Rule

Substitutions

A substitution θ is a finite set of the form {X₁/t₁,...,X_n/t_n} where each X_i is a distinct variable and each t_i is a term (or more generally, a member of some given set of objects) not containing X_i. Each element X_i/t_i is called a binding for X_i. θ may be applied to an formula F to obtain Fθ, the expression obtained from F by similtaneously replacing each occurrence of the X_is in F by t_i. Similarly Sθ may be obtained from a set S of formulae.

A substitution can be applied to another substitution to form their composition. Let θ = {X₁/t₁,...,X_n/t_n} and σ = {Y₁/s₁,...,Y_n/s_n} The variables X_i must be distinct from the variables Y_i, and no X_i can appear in a s_i. The composition θσ is formed by applying σ to the t_i, and combining the two sets. For example, let
    θ = {P1/jim,P2/brother_of(P4)}
and
    σ = {P3/brother_of(P5),P4/geoff}.
Then
    θσ = {P1/jim,P2/brother_of(geoff),P3/brother_of(P5),P4/geoff}.

Unification

A substitution θ unifies a set S of expressions if Sθ is a singleton. A unifier θ is a most general unifier (mgu) for a set S if for each unifier σ of S, there exists a sustitution γ such that σ = θγ.

We are interested in substitutions that unify expressions.

Example

U = { wise(X), wise(brother_of(Y)), wise(brother_of(Z)) }
is unified by θ = {X/brother_of(Z),Y/Z}.

Example
U = { wise(X), wise(brother_of(Y)), wise(brother_of(Z)) } is unified by `θ = {X/brother_of(Z),Y/Z}`.

The disagreement set of a set S of expressions is defined as follows : Locate the left most symbol position at which not all expressions in S have the same symbol and extract from each expression in S the subexpression beginning at that symbol position. The set of all such subexpressions is called the disagreement set.

Example

U = { wise(X), wise(brother_of(Y)), wise(brother_of(Z)) }
has the disagreement set D = {X,brother_of(Y),brother_of(Z)}

Example
U = { wise(X), wise(brother_of(Y)), wise(brother_of(Z)) } has the disagreement set `D = {X,brother_of(Y),brother_of(Z)}`

Unification algorithm for a set U.

Put k=0 and θ₀={}
If Uθ_k is a singleton then θ_k is a mgu for U. Otherwise find the disagreement set D_k of Uθ_k.
If there exist variable V and term t in D_k such that V does not occur in t, then set θ_k+1 = θ_k{V/t}, increment k and loop. Otherwise stop with failure.

Example

U = { wise(X), wise(brother_of(Y)), wise(brother_of(Z)) }

k θ_k Uθ_k D_k

0 {} {wise(X), wise(brother_of(Y)), wise(brother_of(Z))} {X, brother_of(Y), brother_of(Z)}

1 {X/brother_of(Y)} {wise(brother_of(Y)), wise(brother_of(Z))} {Y, Z}
2 {X/brother_of(Z), Y/Z} {wise(brother_of(Z))}

Examples

U Result

{p(X,f(cat)), p(f(Y),f(Y)), p(f(Z),T)} {X/f(cat),Y/cat,T/f(cat),Z/cat}

{p(X,f(cat)), p(f(Y),f(Y)), p(f(dog),Z)} Failure

{p(f(Y),f(Y)), p(f(Z),Z)} Occur check failure

The occur check is omitted in most Prolog implementations.

Resolution

Propositional binary resolution

`C^\| \| L`	`+`	`D^\| \| ~L`
	»	`C^\| \| D^\|`

An intuitive view of binary resolution is as an implementation of modus ponens and modus tolens. Full resolution generalizes the notion.

Propositional full resolution

`C^\| \| L₁ \| ... \| L_n`	`+`	`D^\| \| ~L₁ \| ... \| ~L_m`
	»	`C^\| \| D^\|`

Binary resolution

When performing resolution (and other inference steps) with formulae that contain variables, it is necessary to rename variables such that no variables are common across the two clauses.

`C^\| \| L`	`+`	`D^\| \| ~M`
	`Lθ ≡ Mθ`
	»	`(C^\| \| D^\|)θ`

The two parent clauses resolved against one another, upon the literals that unify. The result is a resolvant. If no literals remain after resolution, the resolvant is FALSE (indicating that the parent clauses contradicted each other). There may be multiple possible resolvant of a pair of parents, by selecting different pairs of literals to resolve upon.

Example

~wise(Z) | wise(brother_of(Z)) + ~wise(X) | ~wise(brother_of(Y)) | taller(X,Y)

1st option

C^| = ~wise(Z)
L = wise(brother_of(Z)) D^| = ~wise(brother_of(Y)) | taller(X,Y)
~M = ~wise(X)

θ = {X/brother_of(Z)}

C^|θ = ~wise(Z)
Lθ = wise(brother_of(Z)) D^|θ = ~wise(brother_of(Y)) | taller(brother_of(Z),Y)
Mθ = wise(brother_of(Z))

(C^| | D^|)θ = ~wise(Z) | ~wise(brother_of(Y)) | taller(brother_of(Z),Y)

2nd option

C^| = ~wise(Z)
L = wise(brother_of(Z)) D^| = ~wise(X) | taller(X,Y)
~M = ~wise(brother_of(Y))

θ = {Y/Z}

D^|θ = ~wise(X) | taller(X,Z) Lθ = wise(brother_of(Z)) Mθ = wise(brother_of(Z))
C^|θ = ~wise(Z)

(C^| | D^|)θ = ~wise(Z) | ~wise(X) | taller(X,Z)

Full resolution

`C^\| \| L₁ \|...\| L_n`	`+`	`D^\| \| ~M₁ \|...\| ~M_m`
	`L_iθ ≡ M_jθ`
	»	`(C^\| \| D^\|)θ`

There may be multiple possible resolvant of a pair of parents, by selecting different combinations of literals to resolve upon.

Example

~wise(Z) | wise(brother_of(Z)) + ~wise(X) | ~wise(brother_of(Y)) | taller(X,Y)

1st option - See binary resolution 1st option

2nd option - See binary resolution 2nd option

3rd option

C^| = ~wise(Z) D^| = taller(X,Y)

L₁ = wise(brother_of(Z)) ~M₁ = ~wise(X) ~M₂ = ~wise(brother_of(Y))

θ = {X/brother_of(Z),Y/Z}

C^|θ = ~wise(Z) D^|θ = taller(brother_of(Z),Z)

L₁θ = wise(brother_of(Z)) M₁θ = wise(brother_of(Z)) M₂θ = wise(brother_of(Z))

(C^| | D^|)θ = ~wise(Z) | taller(brother_of(Z),Z)

Example

wise(brother_of(geoff)) | wise(Z) + ~wise(X) | ~wise(brother_of(Y)) | taller(X,Y)

1st option

L₁ = wise(brother_of(geoff)) ~M₁ = ~wise(X)

θ = {X/brother_of(geoff)}

» wise(Z) | ~wise(brother_of(Y)) | taller(brother_of(geoff),Y)
2nd option
L₁ = wise(brother_of(geoff)) ~M₁ = ~wise(brother_of(Y))
θ = {Y/geoff}
» wise(Z) | ~wise(X) | taller(X,geoff)
3rd option
L₁ = wise(brother_of(geoff)) ~M₁ = ~wise(X) ~M₂ = ~wise(brother_of(Y))
θ = {X/brother_of(geoff),Y/geoff}
» wise(Z) | taller(brother_of(geoff),geoff)
4th option
L₁ = wise(Z) ~M₁ = ~wise(X)
θ = {Z/X}
» wise(brother_of(geoff)) | ~wise(brother_of(Y)) | taller(X,Y)
5th option
L₁ = wise(Z) ~M₁ = ~wise(brother_of(Y))
θ = {Z/brother_of(Y)}
» wise(brother_of(geoff)) | ~wise(X) | taller(X,Y)
6th option
L₁ = wise(Z) ~M₁ = ~wise(X) ~M₂ = ~wise(brother_of(Y))
θ = {Z/brother_of(Y),X/brother_of(Y)}
» wise(brother_of(geoff)) | taller(brother_of(Y),Y)
7th option
L₁ = wise(brother_of(geoff))
L₂ = wise(Z) ~M₁ = ~wise(X)
θ = {Z/brother_of(geoff),X/brother_of(geoff)}
» ~wise(brother_of(Y)) | taller(brother_of(geoff),Y)
8th option
L₁ = wise(brother_of(geoff))
L₂ = wise(Z) ~M₁ = ~wise(brother_of(Y))
θ = {Z/brother_of(geoff),Y/geoff}
» ~wise(X) | taller(X,geoff)
9th option
L₁ = wise(brother_of(geoff))
L₂ = wise(Z) ~M₁ = ~wise(brother_of(Y)) ~M₂ = ~wise(brother_of(Y))
θ = {Z/brother_of(geoff),X/brother_of(geoff),Y/geoff}
» taller(brother_of(geoff),geoff)

Exercise

Find all possible resolvants of

 p(X) | p(f(Y)) | ~q(X,Y)

and

 ~p(f(a)) | ~p(X) | q(c,d)

Answer

Resolution is a sound inference rule

If a set S of clauses is Herbrand satisfiable, then S ∪ {a resolvant from S} is also Herbrand satisfiable.

Proof

Let C^| | L₁ |...| L_n and D^| | ~M₁ |...| ~M_k be two clauses in a set of clauses S, satisfiable by the Herbrand model H, i.e., the two clauses are TRUE in H. Let L_is and M_js be unifiable with most general unifier θ, i.e., the clauses resolve to produce (C^| | D^|)θ.
Let γ any Herbrand universe substitution so that (C^| | L₁ |...| L_n)θγ and (D^| | ~M₁ |...| ~M_k)θγ are ground.

(C^| | L₁ |...| L_n)θγ and (D^| | ~M₁ |...| ~M_k)θγ are TRUE in H.
All L_iθγ and M_jθγ are ground and identical.
(C^| | D^|)θγ is ground.

If C^|θγ is TRUE in H then (C^| | D^|)θγ is TRUE in H.
If C^|θγ is FALSE in H then all L_iθγ is TRUE in H.
If all L_iθγ are TRUE in H then all ~M_iθγ are FALSE in H.
If all ~M_iθγ are FALSE in H then D^|θγ must be TRUE in H.
Hence (C^| | D^|)θσγ is TRUE in H.

As γ is arbitary, the resolvant (C^| | D^|)θ, is TRUE in H, and S ∪ (C^| | D^|)θ is satisfiable.

Example

Consider the resolution between the following two clauses, selected from a Herbrand satisfiable set S. Let H be a Herbrand model of S (e.g., the positive or negative interpretation).

~wise(Z) | wise(brother_of(Z)) + ~wise(X) | ~wise(brother_of(Y)) | taller(X,Y)

C^| = ~wise(Z) D^| = taller(X,Y)
L₁ = wise(brother_of(Z)) ~M₁ = ~wise(X) ~M₂ = ~wise(brother_of(Y))
θ = {X/brother_of(Z),Y/Z}
(C^| | D^|)θ = ~wise(Z) | taller(brother_of(Z),Z)

Let γ be {Z/jim}.

(C^| | L₁)θγ = ~wise(jim) | wise(brother_of(jim))
and
(D^| | ~M₁ | ~M₂)θγ = ~wise(brother_of(jim)) | ~wise(brother_of(jim)) | taller(brother_of(jim),jim)
are TRUE in H.
L_iθγ and M_jθγ = wise(brother_of(jim))
(C^| | D^|)θγ = ~wise(jim) | taller(brother_of(jim),jim) is ground.

If C^|θγ = ~wise(jim) is TRUE in H then (C^| | D^|)θγ = ~wise(jim) | taller(brother_of(jim),jim) is TRUE in H.
If C^|θγ = ~wise(jim) is FALSE in H then L₁θγ = wise(brother_of(jim)) is TRUE in H.
If L₁θγ = wise(brother_of(jim)) is TRUE in H then ~M_jθγ = ~wise(brother_of(jim)) are FALSE in H.
If ~M_jθγ = ~wise(brother_of(jim)) are FALSE in H then D^|θγ = taller(brother_of(jim),jim) must be TRUE in H.
Hence (C^| | D^|)θγ = ~wise(jim) | taller(brother_of(jim),jim) is TRUE in H.
As γ is arbitary, the resolvant (C^| | D^|)θ = ~wise(jim) | taller(brother_of(Z),Z) is TRUE in H.

This theorem shows that all Herbrand models of S are Herbrand models of the resolvant. In other words, resolvants are Herbrand logical consequences of the set. If S ∪ {a resolvant from S} is Herbrand unsatisfiable then the S is Herbrand unsatisfiable.

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 ...

The basic clausal saturation procedure using resolution is :

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

Factoring

Example (showing that binary resolution is not refutation complete)

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

Full resolution
p(X) | q(Y) | q(X) + ~q(a) | ~q(Z) » p(a)
~p(a) + p(a) » FALSE

Binary resolution
Try it, and fail

The Factoring Inference Rule

`C^\| \| L₁ \|...\|L_n`	`+`	Factoring
	`L_iθ = L_jθ`
	»	`(C^\| \| L₁)θ`

Example

~wise(X) | ~wise(brother_of(Y)) | taller(X,Y) | ~wise(brother_of(jim))

1st option
C^| = ~wise(X) | taller(X,Y)
L₁ = ~wise(brother_of(Y))
L₂ = ~wise(brother_of(jim)) + θ = {Y/jim}
» ~wise(X) | taller(X,jim) | ~wise(brother_of(jim))

2nd option
C^| = ~wise(brother_of(Y)) | taller(X,Y)
L₁ = ~wise(X)
L₂ = ~wise(brother_of(jim)) + θ = {X/brother_of(jim)}
» ~wise(brother_of(Y)) | taller(brother_of(jim),Y) | ~wise(brother_of(jim))

3rd option
C^| = ~wise(brother_of(jim)) | taller(X,Y)
L₁ = ~wise(X)
L₂ = ~wise(brother_of(Y)) + θ = {X/brother_of(Y)}
» ~wise(brother_of(jim)) | taller(brother_of(Y),Y) | ~wise(brother_of(Y))

4th option
C^| = taller(X,Y)
L₁ = ~wise(X)
L₂ = ~wise(brother_of(Y))
L₃ = ~wise(brother_of(jim)) + θ = {X/brother_of(jim), Y/jim}
» taller(brother_of(jim),jim) | ~wise(brother_of(jim))

Factoring is used in conjunction with binary resolution to produce full resolution.

All full resolvants of two clauses are formed from all binary resolvants of the two clauses, and all binary resolvants of all factors of the two clauses. Some resolution strategies are complete using binary resolution and factoring, with the application of factoring restricted to certain clauses. This format produces a smaller search space than using full resolution (which in effect allows factoring on all clauses).

Exam Style Questions

What is the most general unifier of the following atoms:
```
p(X,f(Y),Z)
p(T,T,g(cat))
p(f(dog),S,g(W)) 
```
What is the disagreement set of the following atoms:
```
p(X,f(Y),Z)
p(T,T,g(cat))
p(f(dog),S,g(W)) 
```

List all the binary resolvants of the following two clauses:

p(X,f(Y),Z) | p(T,T,g(cat)) | r(X,T) | ~s(Z,T)
~p(f(dog),S,g(W) | s(big,rat) | ~s(small,hamster)

List all the resolvants of the following two clauses:

p(X,f(Y),Z) | p(T,T,g(cat)) | r(X,T) | ~s(Z,T)
~p(f(dog),S,g(W) | s(big,rat) | ~s(small,hamster)

List all the factors of the following clause:

p(X,f(Y),Z) | ~s(Z,T) | p(T,T,g(cat)) | p(f(dog),S,g(W)) | ~s(small,hamster)

One resolvant of the clauses:

p(X,f(Y),Z) | p(T,T,g(cat)) | r(X,T) | ~s(Z,T)
~p(f(dog),S,g(W) | s(big,rat) | ~s(small,hamster)

r(f(dog),f(dog)) | ~s(g(cat),f(dog)) | s(big,rat) | ~s(small,hamster)

Show how that may be formed by factoring and binary resolution.

Prove that if a set S of clauses is Herbrand satisfiable, then S ∪ {a resolvant from S} is also Herbrand satisfiable

Use resolution to derive the empty clause from the set

S = { ~p(X) | ~p(f(X)),
       p(f(X)) | p(X)
      ~p(X) | p(f(X)) }