# CMPS140, Winter 2012, Section 01: Lecture 12

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

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))

Example:
[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*
*0*1
1***
***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.