next up previous
Next: Tuesday, February 22 and Up: Lecture Notes Previous: Tuesday, February 15

February 16, 2000

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.



Randall Holmes
2000-05-05