ex7d-proof-general.txt

> TELL P1
> TELL Q1 ^ R1
> TELL (P1 ^ R1) => S1
> PROOF P1 ^ S1
Proof:
 1. P1                   [Premise]
 2. R1                   [Premise]
 3. ~P1 v ~R1 v S1       [Premise]
 4. ~P1 v ~S1            [Negated Goal]
 5. ~P1 v ~R1            [Resolution on S1: 3, 4]
 6. ~P1                  [Resolution on R1: 2, 5]
 7. ()                   [Resolution on P1: 1, 6]
> TELL P2 => ~(Q2 v R2)
> TELL (~Q2 ^ ~R2) => S2
> PROOF P2 => S2
Proof:
 1. ~P2 v ~Q2            [Premise]
 2. ~P2 v ~R2            [Premise]
 3. Q2 v R2 v S2         [Premise]
 4. P2                   [Negated Goal]
 5. ~S2                  [Negated Goal]
 6. ~Q2                  [Resolution on P2: 1, 4]
 7. ~R2                  [Resolution on P2: 2, 4]
 8. Q2 v R2              [Resolution on S2: 3, 5]
 9. Q2                   [Resolution on R2: 7, 8]
10. ()                   [Resolution on Q2: 6, 9]
> TELL P3 => (S3 ^ ~U3)
> TELL U3
> PROOF ~P3
Proof:
 1. ~P3 v ~U3            [Premise]
 2. U3                   [Premise]
 3. P3                   [Negated Goal]
 4. ~U3                  [Resolution on P3: 1, 3]
 5. ()                   [Resolution on U3: 2, 4]
> TELL (~P4 v Q4) => R4
> TELL S4 v ~Q4
> TELL ~U4
> TELL P4 => U4
> TELL (~P4 ^ R4) => ~S4
> PROOF ~Q4
Proof:
 1. P4 v R4              [Premise]
 2. ~Q4 v S4             [Premise]
 3. ~U4                  [Premise]
 4. ~P4 v U4             [Premise]
 5. P4 v ~R4 v ~S4       [Premise]
 6. Q4                   [Negated Goal]
 7. P4 v ~S4             [Resolution on R4: 1, 5]
 8. S4                   [Resolution on Q4: 2, 6]
 9. ~P4                  [Resolution on U4: 3, 4]
10. ~S4                  [Resolution on P4: 7, 9]
11. ()                   [Resolution on S4: 8, 10]