FOL and Prolog

First Order Logicand Prolog: 

First Order Logic and Prolog Introduction to Artificial Intelligence Henry Kautz Spring 2007

First Order Logic: 

First Order Logic Sentence ::= Atom | (Sentence Connective Sentence) |  Variable . Sentence |   Variable . Sentence |  Sentence Atom ::= Proposition | Predicate(Term, ...) Term ::= Constant | Variable | Function(Term, ...)

First-Order Logic: 

First-Order Logic All men are mortal.  x . (man(x)  mortal(x)) No man is not mortal.   x . (man(x)   mortal(x) ) Everybody has somebody they lean on.  x . (person(x)   y . (person(y)  leans_on(x,y)) A number is less than it’s successor.  n . (number(x)  less_than(x, successor(x)) ) Nothing is less than zero.   x . less_than(x, ZERO)

First-Order Clausal Form: 

First-Order Clausal Form Begin with universal quantifiers (implicit) Rest is a clause No , use function symbols instead Variables in each clause are unique to that clause 'x' in clause 1 is not the same 'x' as in clause 2  x . (man(x)  mortal(x)) man(x)  mortal(x)

Skolem Functions: 

Skolem Functions Begin with universal quantifiers (implicit) Rest is a clause No , use function symbols instead Variables in each clause are unique to that clause 'x' in clause 1 is not the same 'x' as in clause 2  x . (person(x)   y . (person(y)  leans_on(x,y))  x .  y . (person(x)  (person(y)  leans_on(x,y))  x . (person(x)  (person(f(x))  leans_on(x,f(x)))  x .  person(x)  (person(f(x))  leans_on(x,f(x))  x . ( person(x)person(f(x)))  (person(x)leans_on(x,f(x)))  x . person(x)  person(f(x))  x . person(x)  leans_on(x,f(x))

Unification: 

Unification Can resolve clauses if can unify one pair of literals Same predicate, one positive, one negative Match variable(s) to other variables, constants, or complex terms (function symbols) Carry bindings on variables through to all the other literals in the result (Mortal(HENRY)) (Mortal(y)Fallible(y)) (Fallible(HENRY))

Unification with Multiple Variables: 

Unification with Multiple Variables You always hurt the ones you love. Politicians love themselves. Therefore, politicians hurt themselves.  love(x,y)  hurt(x,y) politician(z)  love(z,z) politician(z)  hurt(z,z)

Unification with Multiple Variables: 

Unification with Multiple Variables You always hurt the ones you love. Politicians love themselves. Therefore, politicians hurt themselves.  love(x,y)  hurt(x,y) politician(z)  love(z,z) politician(w)  hurt(w,w) rename 'z' as 'w' so that no clauses have variables with the same name

Why Keep Distinct Variables in Each Clause?: 

Why Keep Distinct Variables in Each Clause? If you hit someone, then you hurt them. If you hurt someone, then you are bad. Therefore: If you hit someone, then you are bad.  hit(x,y)  hurt(x,y)  hurt(y,x)  bad(y) hit(x,x)  bad(x) if you hit yourself then you are bad?!

Why Keep Distinct Variables in Each Clause?: 

Why Keep Distinct Variables in Each Clause? If you hit someone, then you hurt them. If you hurt someone, then you are bad. Therefore: If you hit someone, then you are bad.  hit(x,y)  hurt(x,y)  hurt(w,z)  bad(w) hit(x,z)  bad(x)

Unification with Function Symbols: 

Unification with Function Symbols (Less(a,suc(a))) (Less(b,c) Less(c,d) Less(b,d)) (Less(b,a) Less(b,suc(a))) rename variables: (Less(e,f) Less(e,suc(f))) Less(a,suc(suc(a))) A number is less than its successor 'Less than' is transitive A number is less than the successor of its successor {c/a, d/suc(a)} {e/a,f/suc(a)}

Making FOL Practical: 

Making FOL Practical Barriers to using FOL: Choice of clauses to resolve Huge amount of memory to store DAG Getting useful answers to queries (not just 'yes' or 'no') PROLOG’s answers: Simple backward-chaining resolution strategy – left/right, first to last clause Tree-shaped proofs – no need to store entire proof in memory at one time Extract answers to queries by returning variable bindings

happy.pl: 

happy.pl happy(X) :- rich(X). happy(X) :- loves(X,Y),happy(Y). loves(X,Y) :- spouse(X,Y). loves(X,Y) :- mother(X,Y). rich(bill). spouse(melinda,bill). mother(elaine,melinda). mother(mary,bill). rich(paul). mother(barbara,henry). QUERIES: ?- happy(bill). YES ?- happy(henry). NO ?- happy(Z).

Prolog Interpreter: 

Prolog Interpreter binding_list disprove(literal neglit){ choose (clause c) such that (binding = unify(head(c),neglit)) if (no choice possible){ backtrack to last choice;} for (each lit in body(c)){ binding = binding U disprove(substitute(lit,binding)); } return binding; }

Exercise: The Mini Zebra Puzzle: 

Exercise: The Mini Zebra Puzzle There are three houses in a row on street. Each house is inhabited by a man of a different nationality, who has a different pet, and drinks a different beverage. The Spaniard own a dog. The Ukranian drinks tea. The man in the third house drinks milk. The Norwegian lives next to the tea drinker. The juice drinker owns a fox. The fox is next door to the dog. Question: Who owns the zebra?

Prolog Limitations: 

Prolog Limitations Only handles definite clauses (exactly one positive literal per clause) Cannot express e.g. happy(bill) v happy(henry) Tree-shaped proofs means some sub-steps may be repeatedly derived DATALOG: does forward-chaining inference and caches derived unit clauses Interpreter can get into an infinite loop if care is not taken in form andamp; order of clauses