# Resolution Inference Rules

Resolution is an inference rule (with many variants) that takes two or more parent clauses and soundly infers new clauses. A special case of resolution is when the parent causes are contradictory, and an empty clause is inferred. Resolution is a general form of modus ponens.

## Unification

A substitution θ unifies a set S of expressions if 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}.

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

Unification algorithm for a set U.

• Put k=0 and θ0={}
• If k is a singleton then θk is a mgu for U. Otherwise find the disagreement set Dk of k.
• If there exist variable V and term t in Dk 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 k Dk
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)}
{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.

## Propositional binary resolution

 C| | L + D| | ~L » C| | D|

Example

 i_am_clever | i_will_pass + ~i_am_clever | i_am_happy C| = i_will_pass L = i_am_clever D| = i_am_happy ~L = ~i_am_clever C| | D| = i_will_pass | i_am_happy

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| | L1 | ... | Ln + D| | ~L1 | ... | ~Lm » C| | D|

Example

 i_am_clever | i_will_pass | i_am_clever + ~i_am_clever | i_am_happy C| = i_will_pass Li = i_am_clever D| = i_am_happy ~Li = ~i_am_clever C| | D| = i_will_pass | i_am_happy

## 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| | L1 |...| Ln + D| | ~M1 |...| ~Mm Liθ ≡ Mjθ » (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) L1 = wise(brother_of(Z)) ~M1 = ~wise(X) ~M2 = ~wise(brother_of(Y)) θ = {X/brother_of(Z),Y/Z} C|θ = ~wise(Z) D|θ = taller(brother_of(Z),Z) L1θ = wise(brother_of(Z)) M1θ = wise(brother_of(Z)) M2θ = wise(brother_of(Z)) (C| | D|)θ = ~wise(Z) | taller(brother_of(Z),Z)

Example
 wise(geoff) | wise(brother_of(geoff)) + ~wise(X) | ~wise(Y) | taller(X,Y) 1st option L1 = wise(geoff) ~M1 = ~wise(X) θ = {X/geoff} » wise(brother_of(geoff)) | ~wise(Y) | taller(geoff,Y) 2nd option L1 = wise(brother_of(geoff)) ~M1 = ~wise(X) θ = {X/brother_of(geoff)} » wise(geoff) | ~wise(Y) | taller(brother_of(geoff),Y) 3rd option L1 = wise(geoff) ~M1 = ~wise(Y) θ = {Y/geoff} » wise(brother_of(geoff)) | ~wise(X) | taller(X,geoff) 4th option L1 = wise(brother_of(geoff)) ~M1 = ~wise(Y) θ = {Y/brother_of(geoff)} » wise(geoff) | ~wise(X) | taller(X,brother_of(geoff)) 5th option L1 = wise(geoff) ~M1 = ~wise(X) ~M2 = ~wise(Y) θ = {X/geoff,Y/geoff} » wise(brother_of(geoff)) | taller(geoff,geoff) 6th option L1 = wise(brother_of(geoff)) ~M1 = ~wise(X) ~M2 = ~wise(Y) θ = {X/brother_of(geoff),Y/brother_of(geoff)} » wise(geoff) | taller(brother_of(geoff),brother_of(geoff))

Remember: The variables in a clause are locally quantified. To avoid mistakes, rename variables so that the clauses do not have variables with the same names.

## Resolution is a sound inference rule

If a set S of clauses is Herbrand satisfiable, then S U {a resolvant from S} is also Herbrand satisfiable.
(Or, equivalently, if a set S ∪ {a resolvant from S} of clauses is Herbrand unsatisfiable, then S is Herbrand unsatisfiable.)

Proof

Let C| | L1 |...| Ln and D| | ~M1 |...| ~Mk be two clauses in a Herbrand satisfiable set of clauses S, such that the Lis and Mjs are unifiable with most general unifier θ, i.e. the clauses resolve to produce (C| | D|. Let σ be any Herbrand universe substitution so that (C| | D|)θσ is ground, and γ any Herbrand universe substitution so that (C| | L1 |...| Ln)θσγ and (D| | ~M1 |...| ~Mk)θσγ are ground.

(C| | L1 |...| Ln)θσγ and (D| | ~M1 |...| ~Mk)θσγ are TRUE in a Herbrand model H of S.

• If C|θσγ is TRUE in H then (C| | D|)θσγ is TRUE in H.
• If some Liθσγ is TRUE in H, then all Liθσγ are TRUE in H, and all ~Miθσγ are FALSE in H. Then D|θσγ must be TRUE in H and hence (C| | D|)θσγ is TRUE in H.

As σ and γ are arbitary, the resolvant (C| | D|, is TRUE in H, i.e., S U (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.

 ~wise(Z) | wise(brother_of(Z)) + ~wise(X) | ~wise(brother_of(Y)) | taller(X,Y) C| = ~wise(Z) D| = taller(X,Y) L1 = wise(brother_of(Z)) ~M1 = ~wise(X) ~M2 = ~wise(brother_of(Y)) θ = {X/brother_of(Z),Y/Z} (C| | D|)θ = ~wise(Z) | taller(brother_of(Z),Z)

One possible σ is {Z/jim}, and γ can be {}. Applying θσγ to the two clauses gives:

(C| | L1)θσγ = ~wise(jim) | wise(brother_of(jim))
(D| | ~M1 | ~M2)θσγ = ~wise(brother_of(jim)) | ~wise(brother_of(jim)) | taller(brother_of(jim),jim)

which are both TRUE in H.

If C|θσγ = ~wise(jim) is TRUE in H then (C| | D|)θσγ = taller(brother_of(jim),jim) | ~wise(jim) is TRUE in H.

If L1θσγ = wise(brother_of(jim)) is TRUE in H then ~M1θσγ = ~M2θσγ = ~wise(brother_of(jim)) is FALSE in H and D|θσγ = taller(brother_of(jim),jim) must be TRUE in H. Hence (C| | D|)θσγ = taller(brother_of(jim),jim) | ~wise(jim) is TRUE in H.

As σ and γ are arbitary (C| | D|)θ = taller(brother_of(Z),Z) | ~wise(Z) is TRUE in H.

This theorem shows that all models of S are models of the resolvant. In other words, resolvants are logical consequences of the set. If S U {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 sufficient to:
• Show that S = CNF(Ax U {~C}) is Herbrand unsatisfiable.

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

• Repeatedly do resolution on S and its resolvants, and hope an obviously unsatisfiable set is produced, e.g., one containing an empty clause.

## Factoring

 C| | L1 |...|Ln + Factoring Liθ = Ljθ » (C| | L1)θ

Example

 ~wise(X) | ~wise(brother_of(Y)) | taller(X,Y) | ~wise(brother_of(jim)) 1st option C| = ~wise(X) | taller(X,Y) L1 = ~wise(brother_of(Y)) L2 = ~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) L1 = ~wise(X) L2 = ~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) L1 = ~wise(X) L2 = ~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) L1 = ~wise(X) L2 = ~wise(brother_of(Y)) L3 = ~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.

Example

 Full resolution ~wise(X) | ~wise(brother_of(Y)) | taller(X,Y) + ~wise(Z) | wise(brother_of(Z)) » taller(brother_of(Y),Y) | ~wise(Y) Factoring and Binary resolution ~wise(X) | ~wise(brother_of(Y)) | taller(X,Y) + Factoring » ~wise(brother_of(Y)) | taller(brother_of(Y),Y) ~wise(brother_of(Y)) | taller(brother_of(Y),Y) + ~wise(Z) | wise(brother_of(Z)) » taller(brother_of(Y),Y) | ~wise(Y)

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

1. 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)) ```
2. 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)) ```
3. 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) ```
4. 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) ```
5. 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) `
6. 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) ```
is
`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.
7. Prove that if a set S of clauses is Herbrand satisfiable, then S U {a resolvant from S} is also Herbrand satisfiable
8. 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)) } ```