Chapter 8
Automated Reasoning (Logic Programming)

History:

• numbers
• symbols
• descriptions

want to represent facts

truths in some relevant world

• what are the facts
• how to represent them
  what "formalism" such that one can manipulate and use

Logic review

wff: well-formed formulas (way to represent facts) (e.g. * P U Q is not a wff)

Propositional logic ... propositions

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 (Jackson uses [[propersuperset]] )

Tautologies (same values in truth tables) = (prove)

~ ( 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

P -> Q

P

Q

Modes Tolens

P -> Q

~Q .

~P

~ (~P) <-> P

Very useful

Disjunctive Syllogism

P U Q

~P .

Q

Constructive Dilemma

P -> Q

R -> S

P U R

Q U S

Another

~P -> Q

P -> R

Q U R

Quantifiers

For all [[universal]] There exists [[existential]]

~ [[universal]] x (P (x)) = [[existential]] x ( ~ P (x))

~ [[existential]] x (P (x)) = [[universal]] x ( ~ P (x))

examples of representing statements in logic

All A are B => [[universal]]x (Ax -> B x )

First Order Predicate Calculus (so far only propositional)

statements written as wff

but variables are used to represent objects (only)

Man (Plato)

Man ( x )

Second Order Predicate Calculus

variables are used to represent ??

Computable Predicates (augmentation)

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

Proofs in Logic

* many sequences (for the same goal statement) are possible

* different proof methods exist (e.g., resolution, natural deduction)

Theorem Proving

* represent statements in predicate logic

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

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

* clause form

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

Example:

It is not true that for all x:Px -> Qx ~[[universal]]x : Px -> Qx

There exists an x such that ~ (Px -> Qx) [[existential]]x: ~ (Px -> Qx)

There exists an x such that ~(~Px U Qx) [[existential]]x: ~(~Px U Qx)

DeMorgans says this is Px * ~Qx

Notice this is NOT equivalent to: [[universal]]x: Px -> ~Qx

or There exists x where Px ->~Qx

So "Gentlemen are not always rich" can be said as

"It is not true that gentlemen are always rich"

Which reduces to "There exists someone who is a gentleman and who is not rich"

Convert to Clause form (CNF):(simple example: pg 145)

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)

[[universal]]x: P(x) U [[universal]]x: Q(x) converts to [[universal]]x: P(x) U [[universal]]y: Q(y)

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

5. Eliminate existential qualifiers [[existential]]

* Skolem functions "Magic(x) functions"

[[universal]]x [[existential]]yfather-of(y,x) value of y depends on x so (y is the father of x)

[[universal]]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

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)

Clausal Form - at this time, all are ORs. Organize so clauses with negation go on right so:

{{ ~p, p, q}, {~q, p, q}} becomes:

p,q <- p

p,q <- q (notice, if p is true, then ~p is false; consider left-side then)

Causal Normal Form and clauses (example - Jackson pg 145)

Horn Clause form says only one clause can be in conclusion (which is left hand side), so clauses

that look like p <- q1, ... , qn

are written p :- q1, ... , qn

This would then read

If q1 and q2 and ... ,and qn are true, then p is true

OR

P if q1 and q2 and ... ,and qn are true

Representation in Logic vs Prolog

Logic

[[universal]]x: pet(x) [[intersection]] small(x) -> apartmentpet(x)

[[universal]]x: cat(x) [[union]] dog(x) -> pet(x)

[[universal]]x: poodle(x) -> dog(x) [[intersection]] small(x)

poodle(fluffy)

Prolog

apartmentpet(x) :- pet(), small(x)

pet(x) :- cat(x)

pet(x) :- dog(x)

dog(x) :- poodle(x)

small(x) :- poodle(x)

poodle(fluffy)

A key difference between logic and the PROLOG representation is that the PROLOG interpreter has a fixed control strategy, and so the assertions in the PROLOG program define a particular search path to an answer to any question. (compare to rule-based)

PROLOGs reasoner is based on the resolution principle

Resolution Theorem Proving

pre: logical representation of facts

1. convert to clause form (example - Jackson: pg 146)
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

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 vi -> f(...)

(z/y)(y/x): apply rightmost,then take result and continue

Example:

hate(x,y)

hate(marcus, z)

binds (unifies)

(marcus/x, z/y)

Examples: Marcus (CNF) and Prolog (Horn (page 149 (facts),153 (resolution)))

PROLOG:

• Begin with a problem statement, a goal to be proved
• Look for assertions that can prove the goal
  • Consider facts that can prove the goal directly
  • Consider any rule whose head matches the goal
• Reason backward from that goal until a path is found that terminates with assertions in the program
• Consider paths using a depth-first strategy and using backtracking

Example : ? - apartmentpet(x)

Note: In pure PROLOG, logical negation cannot be represented. So it is not possible to encode directly the logical assertion: [[universal]]x: dog(x) -> ~ cat(x)

Instead negation is represented implicitly by the lack of assertion. If the prolog program were given

?- cat(fluffy)

it would return FALSE since it is unable to prove that Fluffy is a cat. Unfortunately, this program returns the same answer when given

?- cat(Mittens)

even though it knows nothing about Mittens and specifically nothing that might prevent Mittens from being a cat.

Negation by failure requires that we make what is called the closed world assumption, which states that all relevant, true assertions are contained in our knowledge base or are derivable from the assertions so contained.

(Problems with incomplete knowledge bases)

Logic:

Questions to consider: