Automated DeductionResolutionSlide 3Converting FOL sentences to CNFExampleconvert to CNFSlide 7Slide 8Backward-chainingSlide 10Slide 11Map-Coloring in PrologNegation in PrologForward-ChainingSlide 15Slide 16Slide 17Automated Deduction•resolution (Otter)•backward-chaining (Prolog)•forward-chaining (Rete, Clips, Jess)•also called “theorem provers” or “inference engines”•example application:–think about using rules to infer “right-of-way” in a driving simulationResolution•first-order (with unification)–(ab)(a’c) ᅡ (b”c”)–where =unifier(a,a’) and b”=apply(b,c”=apply(c,•exampleX works_for(X,government) v receives_pension(X)–works_for(kate,government) v works_for(kate,walmart)–works_for(kate,walmart) v receives_pension(kate)– ={X/kate}•resolution is refutation-complete for FOL–must convert all sentences to CNF–a ground instance of a clause is formed by instantiating all variables with some constant•P(X,Y)vQ(Y,Y) : {P(sam,bill)vQ(bill,bill); P(sam,joe)vQ(joe,joe)...}–Herbrand’s Theorem: if a set of sentences is unsatisfiable, then there exists a set of ground (propositional) instances that is unsatisfiable–Ground Resolution Theorem: if a set of propositional clauses is unsatisfiable, then there is a finite derivation of the empty clause–Lifting Lemma: If there is proof of the empty clause using ground instances, then there is parallel proof using the original clauses with variables (using unification)Converting FOL sentences to CNF•eliminate implications (ab ᅡ ab)•move neg. inwards (DeMorgans’ Laws, x P ᅡ x P)•standardize variables apart (if X is used in multiple quantifiers, replace instance with X1, X2...)•skolemization (replace  vars with *new* constants)•drop universal quantifiers •distribute  over •break conjunctions into separate clauses•“Everyone who loves all animals is loved by someone.”x (y animal(y)loves(x,y))y loves(y,x)•“The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missles, and all of its missles were sold to it by Colonel West, who is an American.”•Prove that Colonel West is a criminal.x,y,z american(x)&weapon(y)&sells(x,y,z)&hostile(z) criminal(x)x owns(nono,x)&missle(x)x owns(nono,x)&missle(x)sells(west,x,nono)x missle(x)weapon(x)x enemy(x,america)hostile(x)•american(west), enemy(nono,america)•negation of query: criminal(west)Exampleconvert to CNFx,y,z american(x)&weapon(y)&sells(x,y,z)&hostile(z) criminal(x){american(x1),weapon(y1),sells(x1,y1,z1),hostile(z1), criminal(x1)}x missle(x)weapon(x){missle(x2),weapon(x2)}x owns(nono,x)&missle(x)sells(west,x,nono){owns(nono,x3), missle(x3),sells(west,x3,nono)}x owns(nono,x)&missle(x){owns(nono,M),missle(M)} – M is a skolem constantx enemy(x,america)hostile(x){enemy(x4,america),hostile(x4)}•american(west), enemy(nono,america),criminal(west)•maybe thousands of clauses – difficult search•search strategies: which clauses to resolve?–unit preference: •one clause must be of length 1•guarantees to reduce length of other clause (toward 0)–set of support:•one clause must be from the sos, e.g. negated query•“source” of the unsatisfiability–input resolution:•one clause must be from the input (KB or query)–linear resolution•one clause must be from negated query OR a successor derived from it•complete•Otter – a real-world resolution theorem proverBackward-chaining•recall: subgoal stack–try to reduce to facts; might have to back-track•KB must be in Horn-clause form•in FOL, use unification–for popped subgoal, try to unify with fact or head of some clause•Prolog – a practical implementation of a back-chaining theorem prover–funky syntax–can be used for many solving many problems–learn how to use back-chaining as “computational model”–widely employed for expert systems, intelligent agents, control applications...•Prolog syntax–facts: predicate(args,...).–rules: •no quantifiers, variables in capital letters, •written backwards, “:-” means “” , read as “if”•“,” means conjunction; no disjunctionX dog(X)  mammal(X)•mammal(X) :- dog(X). •canPlay(Child) :- hasEaten(Child,dinner),finished(Child,homework).–also support for strings, lists, numbers...•Problem solving by back-chaining•combinatorial enumeration/search (unbound variables)•often interested in variable binding of solutionfather(X,Y) :- parent(X,Y),male(X).mother(X,Y) :- parent(X,Y),female(X).sibling(X,Y) :- parent(Z,X),parent(Z,Y).grandparent(X,Y) :- parent(X,Z),parent(Z,Y).uncle(X,Y) :- parent(Z,Y),sibling(X,Z),male(X).male(john). male(sam). male(joe). male(bill). female(sue). female(ellen).parent(sam,john), parent(ellen,john). parent(ellen,joe). parent(sam,joe).parent(sue,bill). parent(al,sam). parent(sue,ellen).query: ?- uncle(bill,john).yes.query: ?- uncle(sue,john).fail.query: ?- grandparent(X,john).X=al; X=sueMap-Coloring in Prologcolor(red).color(green).color(blue).color(yellow).valid_coloring(A,B,C,D,E) :- color(A),color(B),color(C),color(D),color(E), not A=B, not A=C, not A=D, not A=E, not B=C, not B=D, not C=D, not D=E.•effectively enumerates all combinations of colors and tests them for consistency.•will try A=red, B=red, C=red, D=red, E=red first •fail, because doesn’t satisfy not A=B.•then back-track to A=red, B=red, C=red, D=red, E=green, which fails not A=C.•and so on, until reach A=red, B=green, C=blue, D=yellow, E=green •not very efficient, but illustrative of the kind of combinatorial problem-solving that can be simulated via back-chainingNegation in Prolog•Can have negative literals in antecedents.•not strict FOL semantics•“negation-as-failure”•...,not p(X),... means try to prove p(X) (by back-chaining with current variable bindings)–if cannot prove it, then proceed–if can prove it, then fail and back-track•very handy – allows default inference, compact KB•canFly(X) :- bird(X),not broken(wings(X)).•bird(X) :- canary (X).•bird(X) :- penguin(X).•bird(X) :- eagle(X).•canary(tweety). penguin(opus). eagle(sam).•broken(wings(opus)).?- canFly(B).B=sam.B=tweety.Forward-Chaining•requires Horn-clause