The take home test has been distributed. It is due on February 22. You will receive credit for lab 2 if you use the theorem prover to do problem 1 on the take-home.

READ THIS: There is a typographical error in the take-home (which makes the solution trivially easy); in problem 1, the last conjunct has ands where it should have ors. The correct form is now posted (as Postscript) on my web page. I also include it here:

Convert the formula

(P | ~Q | R | ~S) & (~P | Q | ~R | S) & (P | ~Q | ~R | ~S)

to DNF (I tried to include it in the fancy type-face, but that aspect of latex2html is not working at the moment).

Here is the proof I promised to post. I plan to post more solved homework 5 problems as notes for this day, since we spent it on review. #20 homework 5, using Grantham's rule of disjunction elimination, which I call ``proof by cases''. A | (B & C) |- (A | B) & (A | C) 1. A | (B & C) premise Goal: (A | B) & (A | C) | 2. A subpremise (case 1 of a proof by cases using line 1) | Goal: (A | B) & (A | C) | Goal: A | B | 3. A | B disj. intro. line 2 (Grantham's rule, my special case) | Goal: A | C | 4. A | C disj. intro. line 2 | 5. (A | B) & (A | C) c.i. lines 3,4 notice that this ends one box and another begins | 6. B & C subpremise (case 2 of a proof by cases using line 1) | Goal: (A | B) & (A | C) | Goal: A | B | 7. B c.e., line 6 | 8. A | B disj. intro. line 7 | Goal: A | C | 9. C c.e., line 6 | 10. A | C disj. intro. line 7 | 11. (A | B) & (A | C) c.i. lines 8,10 Here's where the proof by cases pays off: 12. (A | B) & (A | C) proof by cases, line 1, lines 2-5, lines 6-11 For comparison I include a solution not using proof by cases: 1. A | (B & C) premise Goal: (A | B) & (A | C) Goal: A|B | 2. ~A premise (for disj. intro) | Goal: B | 3. B & C disj. elim. lines 2,1 | 4. B c.e. line 3 5. A | B disj. intro lines 2-4 Goal: A|C | 6. ~A premise (for disj. intro) | Goal: C | 7. B & C disj. elim. lines 6,1 | 8. C c.e. line 3 9. A | C disj. intro lines 2-4 10. A|B & A|C c.i. lines 5,9 This proof is slightly shorter but the first one may be considered more intuitive by some. This proof admits the following alarming refinement: 1. A | (B & C) premise Goal: (A | B) & (A | C) Goal: A|B | 2. ~A premise (for disj. intro) | Goal: B | 3. B & C disj. elim. lines 2,1 | 4. B c.e. line 3 | 5. C c.e. line 3 6. A | B disj. intro lines 2-4 7. A | C disj. intro lines 2-5 8. A|B & A|C c.i. lines 6,7 The reason that this is ``alarming'' is that the subproof in the box is ``reused'' to prove two different conclusions. This is permitted by our rules, but requires a good understanding of them to carry off without error! More sample solutions may appear in this space.