Logic review

wff: well-formed formulas (way to represent facts)

(e.g. * P U Q is not a wff)

Propositional logic

It is raining RAINING

It is sunny SUNNY

If it is raining then it is not sunny

RAINING -> NOT(SUNNY)

Represent as P and Q: Truth Tables

AND	OR	Implication
P * Q	P U Q	P ==> Q

Do table for ((P * Q) -> R) -> (P -> (Q -> R))

Tautologies (same values in truth tables) = (equivalent - prove it with truth tables) The statements below are equivalent (deMorgan's)

~ ( P U Q)   =  ~P * ~Q            ~( P * Q)  =  ~P U ~Q

Distributive Law

P U ( Q * S) = (P U Q) * (P U S)

P * (Q U S) = (P * Q) U (P * S)

Associative Law

P U Q U S (order is irrelevant)

deMorgans

~ (P U Q) = ~P * ~Q

~ (P * Q) = ~P U ~Q

Modes Ponens         Modes Tolens

P -> Q                    P --> Q

P                                ~Q        

Q                                ~P

~ (~P) <-> P

Very useful

Disjunctive Syllogism

P U Q

~P        

Q

Constructive Dilemma

P --> Q                    ~P --> Q

R --> S                       P --> R     

P U R                        Q U R

Q U S

First Order Predicate Calculus

statements written as wff

but variables are used to represent objects (only)

Man (Plato)

Man ( x )

Quantifiers

For all            There exists

~ x (P (x))  =  x ( ~ P (x))

~ x (P (x))  =  x ( ~ P (x))

examples of representing statements in logic

All A are B => x (A_x -> B _x )

Second Order Predicate Calculus

variables are used to represent ??

Computable Predicates (augmentation)

gt(1,0) ... do not want to write all truths

Theorem Proving

* represent statements in predicate logic - not always easy!

(note the difference between p -> q and p * q

p -> q is still a true statement is p if False)

p -> q  =  ~p U q (show tautology)

Resolution Theorem Proving

pre: logical representation of facts

1. convert to clause form

2. negate S (statement to prove) and convert to clause form

3. resolve

• assume negation of S

• show that axioms and assumed negation determine something to be true that cannot be true

• conclude assumption of negation is false

• therefore S is true

Remember Constructive Dilemma

~P --> Q

  P --> R     

Q U R

Convert to Clause form to do algorithmically, need a representation to work with(conjunctive normal form):

example proof

1. p -> q = ~p U Q

2. reduce scope of ~ using

• * ~(~p) = p

• * DeMorgans ~(p * q) = ~p U ~q , etc.

• * quantifiers

3. Standardize variables so that each quantifier binds a unique variable (i.e., rename)

x: P(x) U x: Q(x) converts to x: P(x) U y: Q(y)

4. Move all variables to the left (OK since each unique)

5. Eliminate existential qualifiers

* Skolem functions "Magic(x) functions"

father-of(y,x) value of y depends on x so (y is the father of x)

father-of(S2(x), x)

If someone gives you some particular object x, you will always be able to name an object y that makes the expression TRUE.

I.e., there is a function that takes argument x and returns a proper y.

There must be one argument for each universally quantified variable whose scope contains the existentiallly quantified variable that the Skolem function replaces.

6. Drop the prefix (for all: all universal...so...)

7. Convert to a conjunction (and) of disjuncts

* simply remove parenthesis or

* distributive law

8. Separate clauses of each conjunct

9. Standardize apart the variables in the set of clauses

(rename the variables so no not meant "connections")

(e.g. like #3 but now in the set of clauses)

Unification:

For propositional logic, no variables

For First Order Predicate Calculus, we need matching and binding of variables

L ~L (contradiction)

man(Henry) ~man(Henry) (contradiction)

man(Henry) ~man(Spot) (~ contradiction)

man(Henry, t1) man(Henry, 13)

(predicate argument1 argument2 ... argumentn)

1. predicates match?

then check arguments

2. variables

• constants vi -> c

• variables v1 -> v2

• functions not containing variables v_i -> f(...)

P(y,z)

I can replace x with y or y with x (just dummies)

but must be consistent.

y/x says substitute y for x. (note: cannot also do z/x)

P(y,y)

P(y,z) with unification composition of (z/y)(y/x)

(apply rightmost,then take result and continue)

Example:

hate(x,y)
hate(marcus, z)

binds (unifies)
(marcus/x, z/y)

Green's trick

Which resolution to try (proof is exponential)

1) shortest clause

2) start with negated assumption

(want to say something about this inparticular)

3) breadth-first (complete, will find if exists) (combinitoric)

(resolve all clauses so far

       use these results

resolve again..)