Resolution

The idea of resolution is simple: if we know that

This line of reasoning is formalized in the Resolution Tautology: 

      (p OR q) AND (NOT p OR r) -> q OR r

In order to apply resolution in a proof:

  1. we express our hypotheses and conclusion as a product of sums (conjunctive normal form), such as those that appear in the Resolution Tautology.

  2. each maxterm in the CNF of the hypothesis becomes a clause in the proof.

  3. we apply the resolution tautology to pairs of clauses, producing new clauses.

  4. if we produce all the clauses of the conclusion, we have proven it.

Proof with Resolution

Given the following hypotheses:

  1. If it rains, Joe brings his umbrella (r -> u)
  2. If Joe has an umbrella, he doesn't get wet (u -> NOT w)
  3. If it doesn't rain, Joe doesn't get wet (NOT r -> NOT w)
prove that Joes doesn't get wet (NOT w)

We first put each hypothesis in CNF:

  1. r -> u == (NOT r OR u)
  2. u -> NOT w == (NOT u OR NOT w)
  3. NOT r -> NOT w == (r OR NOT w)

We then use resolution on the hypotheses to derive the conclusion (NOT w): 

   1. NOT r OR u        Premise
  
   2. NOT u OR NOT w    Premise
  
   3. r OR NOT w        Premise
  
   4. NOT r OR NOT w    L1, L2, resolution
  
   5. NOT w OR NOT w    L3, L4, resolution
  
   6. NOT w             L5, idempotence
  
   7. QED

Proofs by Contradiction using Resolution

We can combine resolution with proof by contradiction (where we assert the negation of what we wish to prove, and from that premise derive FALSE) to direct our search towards smaller and smaller clauses, with the goal of producing FALSE.

Proof by contradiction: 

      (NOT p -> 0) == p

We use proof by contradiction to drive our search for a proof; we are looking for the smallest possible goal clause (false), so any use of equivalences or resolution that brings us to simpler expressions is working towards that goal.

We can redo the previous proof (about Joe and his umbrella) using proof by contradiction with resolution: 

   1. NOT r OR u        Premise
  
   2. NOT u OR NOT w    Premise
  
   3. r OR NOT w        Premise
  
   4. w                 Negation of conclusion
  
   5. NOT r OR NOT w    L1, L2, resolution
  
   6. NOT w OR NOT w    L3, L5, resolution
  
   7. NOT w             L6, idempotence
  
   8. FALSE             L4, L7, resolution

Proof by Resolution: Example 1

If either C173 or C220 is required, then all students will take computer science. C173 and C240 are required. Prove that all students will take computer science.

We formalize the proof as follows: 

   P1. (C173 OR C220) -> ACS
   P2. C173
   P3. C240
   Prove: ACS

We then rewrite our hypotheses in conjunctive normal form: 

   P1: (NOT C173 OR ACS) (NOT C220 OR ACS)
   P2: C173
   P3: C240

Then we use proof by contradiction, by asserting the clauses of the premises and the negation of the conclusion, and deriving false. 

   1. NOT C173 OR ACS    Premise
   2. NOT C220 OR ACS    Premise
   3. C173               Premise
   4. C240               Premise
   5. NOT ACS            Negation of conclusion
   6. NOT C173           L1, L5, resolution
   7. FALSE              L3, L6, resolution

Proof by Resolution: Example 2

Either Heather attended the meeting or Heather was not invited. If the boss wanted Heather at the meeting, then she was invited. Heather did not attend the meeting. If the boss did not want Heather there, and the boss did not invite her there, then she is going to be fired. Prove Heather is going to be fired. 

   1. A OR NOT I     Premise
  
   2. NOT W OR I     Premise
  
   3. NOT A          Premise
  
   4. W OR I OR F    Premise
  
   5. NOT F          Negation of conclusion
  
   6. W OR I         L4, L5, resolution
  
   7. I              L2, L6, resolution, idempotence
  
   8. A              L1, L7, resolution
  
   9. FALSE          L3, L8, resolution

Proof by Resolution: Example 3

Either taxes are increased or if expenditures rise then the debt ceiling is raised. If taxes are increased, then the cost of collecting taxes rises. If a rise in expenditures implies that the government borrows more money, then if the debt ceiling is raised, then interest rates increase. If taxes are not increased and the cost of collecting taxes does not increase then if the debt ceiling is raised, then the government borrows more money. The cost of collecting taxes does not increase. Either interest rates do not increase or the government does not borrow more money.

Prove either the debt ceiling isn't raised or expenditures don't rise. 

   1. T OR NOT E OR D              Premise
  
   2. NOT T OR C                   Premise
  
   3. (E AND NOT G) OR NOT D OR I  Premise
  
   4. T OR C OR NOT D OR G         Premise
  
   5. NOT C                        Premise
  
   6. NOT I OR NOT G               Premise
  
   7. D AND E                      Negation of conclusion
  
   8. (E AND NOT G) OR I           L3, L7, resolution
  
   9. C OR NOT D OR G              L2, L4, resolution
  
  10. C OR G                       L7, L9, resolution
  
  11. G                            L5, L10, resolution
  
  12. NOT I                        L6, L11, resolution
  
  13. E AND NOT G                  L8, L12, resolution
  
  14. NOT G                        L13, tautology
  
  15. FALSE                        L11, L14, contradiction