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^\|`

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 put θ_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 ommitted in most Prolog implementations.

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.

Binary resolution

`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)

Resolution is a sound inference rule

The Quest for Logical Consequence

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

Show that S' = A U {~C} is unsatisfiable.

S' is unsatisfiable iff S = CNF(S') is unsatisfiable

Show that S is unsatisfiable.

If a set S U {a resolvant from S} of clauses is unsatisfiable, then S is unsatisfiable, so

Apply the basic saturation procedure with resolution as the inference rule, and hope an obviously unsatisfiable set is produced, e.g., one containing FALSE

Example

If you are taller than someone then you are wise. Being taller is a transitive relationship. Eric's brother is taller than Bruce. Bruce is taller than Eric. Prove that there is someone's brother who is wise, and is taller that both Bruce and Eric.

The ANL Loop

The ANL loop is a flexible algorithm for controlling the generation of inferred clauses.

Let CanBeUsed = {}
Let ToBeUsed = Input clauses
While Refutation not found && ToBeUsed not empty
    Select the ChosenClause from ToBeUsed
    Move the ChosenClause to CanBeUsed
    Infer all possible clauses using the ChosenClause and other clauses from CanBeUsed.
    Add the inferred clauses to ToBeUsed

Depending on how the ChosenClause is selected from the ToBeUsed set, different search strategies can be implemented. The "Least Symbol Count" strategy selects the clause with the least number of symbols from the ToBeUsed set, thus aiming for an empty clause.

Example

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

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

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(S,W)

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)) }

Write out the ANL loop algorithm.
Show the execution of the ANL loop to derive the empty clause from:
```
S = { ~r(Y) | ~p(Z),
      p(b),
      r(a), 
      p(S) | ~p(b) | ~r(S),
      r(c) } 
```
Use any selection strategy you want, and number the chosen clause at each iteration.