The idea of resolution is simple: if we know that

- p is true or q is true
- and we also know that p is false or r is true
- then it must be the case that q is true or r is true.

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:

- we express our hypotheses and conclusion as a product of sums
(conjunctive normal form),
such as those that appear in the Resolution Tautology.
- each maxterm in the CNF of the hypothesis
becomes a
*clause*in the proof. - we apply the resolution tautology to pairs of clauses,
producing new clauses.
- if we produce all the clauses of the conclusion, we have proven it.

Given the following hypotheses:

- If it rains, Joe brings his umbrella (r -> u)
- If Joe has an umbrella, he doesn't get wet (u -> NOT w)
- If it doesn't rain, Joe doesn't get wet (NOT r -> NOT w)

We first put each hypothesis in CNF:

- r -> u == (NOT r OR u)
- u -> NOT w == (NOT u OR NOT w)
- 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

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

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

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

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