|
Both disjunction rules are illustrated by the derivation at the right, in which one grouping of a three-part disjunction is shown to entail the other. Choices between the two ways of planning for a goal disjunction were made at stages 2, 3, 5, 6, and 7 in accordance with the rules of thumb given above. Each choice helped to shorten the derivation—though only by a few steps. The derivation is contrived to provide several examples of this rule; we might have instead planned for the initial goal at stage 1 before exploiting the premise rather than planning for it later in each of three gaps.
|
|
| │A ∨ (B ∨ C) | 1 |
| ├─ | |
| ││A | (4) |
| │├─ | |
| │││¬ C | |
| ││├─ | |
| ││││¬ B | |
| │││├─ | |
| ││││● | |
| │││├─ | |
| 4 QED | ││││A | 3 |
| ││├─ | |
| 3 PE | │││A ∨ B | 2 |
| │├─ | |
| 2 PE | ││(A ∨ B) ∨ C | 1 |
| │ | |
| ││B ∨ C | 5 |
| │├─ | |
| │││B | (8) |
| ││├─ | |
| ││││¬ C | |
| │││├─ | |
| │││││¬ A | |
| ││││├─ | |
| │││││● | |
| ││││├─ | |
| 8 QED | │││││B | 7 |
| │││├─ | |
| 7 PE | ││││A ∨ B | 6 |
| ││├─ | |
| 6 PE | │││(A ∨ B) ∨ C | 5 |
| ││ | |
| │││C | (10) |
| ││├─ | |
| ││││¬ (A ∨ B) | |
| │││├─ | |
| ││││● | |
| │││├─ | |
| 10 QED | ││││C | 9 |
| ││├─ | |
| 9 PE | │││(A ∨ B) ∨ C | 5 |
| │├─ | |
| 5 PC | ││(A ∨ B) ∨ C | 1 |
| ├─ | |
| 1 PC | │(A ∨ B) ∨ C | |
|