# Comments on resolution

### Resolution with propositional calculus or
ground clauses (i.e. clauses without variables)

parent clauses | resolvent | comments |

P, ¬P ∨ Q | Q | this is the same as
Modus Ponens |

¬P ∨ Q, ¬Q ∨ R | ¬P ∨ R |
This is often called Chaining. The positive and negative literals
cancel out. |

P ∨ Q, ¬P ∨ Q | Q | Merge (or Factoring)
(Q ∨ Q collapses to Q) |

P ∨ Q, ¬P ∨ ¬Q | Q ∨ ¬Q |
Tautology. This is a dead end, since there is no other clause that
can be resolved with it. |

P ∨ Q, ¬P ∨ ¬Q | P ∨ ¬P |
Tautology. This is a dead end, since there is no other clause that
can be resolved with it. |

P, ¬P | NIL | Contradiction. This is what we
are looking for. |

### Example

You are given the following expressions:
P ∧ Q ∧ R → S
¬Q → R
¬S → P

and you are asked to prove S

- First we need to transform the expressions into clause form.
1. ¬P ∨ ¬Q ∨ ¬R ∨ S
2. Q ∨ R
3. S ∨ P

- Next, we negate what we are trying to prove, transform it to
clause form, and add it to the knowledge base.
4. ¬S

- We use resolution to try to produce a contraddiction.
resolve 3. S∨P with 4 ¬S
obtain 5. P
resolve 5. P with 1. ¬P&or¬Q&or¬R∨S
obtain 6. ¬Q∨¬R∨S
resolve 6. ¬Q∨¬R∨S with 2. Q∨R
obtain 7. ¬R∨S∨R = True

We can try resolving other clauses, such as
resolve 1. ¬P∨¬Q∨¬R∨S with 4. ¬S
obtain 8. ¬P∨¬Q∨¬R
resolve 8. ¬P∨¬Q∨¬R with 3. S∨P
obtain 9. ¬Q∨¬R∨¬S (this is the same as 6)

but there is no other step we can take to produce the empty clause, so
we fail to prove a contraddiction. Since this example is in propositional
calculus, and propositional calculus is decidable (i.e. there is a
procedure for deciding if an expression is entailed or not) failure
to prove an expression means the expression is not entailed by the
knowledge base.
We would not be able to make the same statement if we were to use
predicate calculus, since predicate calculus is
semi-decidable (i.e. if a sentence is entailed we can prove it, but not
the reverse).

Suppose now you are asked to add a minimal set of clauses to make S
derivable. What would that set be?
A way of answering is by constructing the truth table:
P Q R S Q∨R S∨P ¬P∨¬Q&or¬R∨S
1 T T T T T T T
2- T T T F T T F
3* T T F T T T T
4* T T F F T T T
5 T F T T T T T
6 T F T F T T T
7- T F F T F T T
8- T F F F F T T
9 F T T T T T T
10- F T T F T F T
11* F T F T T T T
12- F T F F T F T
13 F F T T T T T
14- F F T F T F T
15- F F F T F T T
16- F F F F F F T

Since we know the sentences in the knowledge base are true, we can
eliminate from consideration lines 2, 7, 8, 10, 12, 14, 15, 16 (lines
marked with a -).
As we can see from the remaining table, the knowledge given is not
sufficient to prove S (i.e. there are still cases where S is False.)

P Q R S Q∨R S∨P ¬P∨¬Q&or¬R∨S
1 T T T T T T T
3* T T F T T T T
4* T T F F T T T
5 T F T T T T T
6 T F T F T T T
9 F T T T T T T
11* F T F T T T T
13 F F T T T T T

If we add to the knowledge base R, we can eliminate lines 3, 4, and 11
(lines marked with a *).
Still we cannot prove S (look at line 6, where S is false).
We would need to add another expression, such as Q.