Comments on resolution

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

parent clauses	resolvent	comments
P, ¬P ∨ Q	Q	Modus Ponens
¬P ∨ Q, ¬Q ∨ R	¬P ∨ R	Chaining
P ∨ Q, ¬P ∨ Q	Q	Merge (or Factoring) (Q ∨ Q collapses to Q)
P ∨ Q, ¬P ∨ ¬Q	Q ∨ ¬Q	Tautology
P ∨ Q, ¬P ∨ ¬Q	P ∨ ¬P	Tautology. This is a dead end, since there is no other clause that can be resolved with this.
P, ¬P	NIL	Contraddiction

Example

Suppose you are given the following expressions:

P ∧ Q ∧ R → S
¬Q → R
¬S → P

and you are asked to prove

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.