CMPS140, Winter 2012, Section 01: Lecture 12

  4 Propositional Proof Techniques for Prop Logic:
       Truth Tables
       Sat Matrices
       Existential Graphs.

Read about  Resolution in Chapter 7-8 of text.

Existential Graphs:

   Logic       EGs
     P          P
     ~P        (P)
     P and Q    P Q
     P or Q     ((P) (Q))
     P => Q     (P (Q))

Idea:  Circle Goal derive an empty circle on the sheet!

Rules:  ((x)) ---> x.
      x ((x)x)     ---> x (())

       x can kill inner copy at any level of nesting:   x   (z(x y)) --> (z(y))

[A => (B or C)) and ~C  and B => D  therefore A => D.

   in EGs:    ((A (((B) (C)))) (C) (B (D))      ((A (D)))   )

    Negate goal:
       (((A (((B) (C)))) (C) (B (D))      ((A (D)))   ))
     Remove Double Negation
       (A (((B) (C)))) (C) (B (D))      ((A (D)))

     Remove double negation:
        (A (B) (C))    (C) (B (D))     A (D)

     Kill A:
        ((B) (C))   (C) (B (D)) A (D)

     KILL (D):    ((B) (C)) (C)   (B) A (D)

     KILL (B):
                 ((C))   (C)  (B) A (D)

     KILL   (C):      () (C)   (B) A (D)

     We are done since there is a () on the sheet!!!

In resolution:
     First convert to CNF:
       1. ~A or B or C   given
       2. ~C               given
       3. ~B or D          given
        4. A                drom negated goal
       5 ~D                from negated goal

       6. ~B               3,5
       7. ~A or C          1,6
       8. C                4,7
       9. {}               2,8  we have derived {} so we are done!

SAT matrix     011*
              ***0     which is UNSAT = contradiction!

All elephants speak the same languages:
 Represent in FOL:
      Forall(e) Forall(l)([ Elephant(e) and Language (l)]  =>
                         [Speak(e,l) => Forall(y) [elephant(y) => Speak(y,l)]]).

P |= Q means Q can be derived from P, means that Q is true whenever P is.