Chapter9.ppt

1、Inference in first-order logic,Based on AIMA PPT slides,2,October 27, 2020,Outline,Reducing first-order inference to propositional inference Unification Generalized Modus Ponens Forward chaining Backward chaining Resolution,3,October 27, 2020,Universal instantiation (UI),Every instantiation of a uni

2、versally quantified sentence is entailed by it: v Subst(v/g, ) for any variable v and ground term g E.g., x King(x) Greedy(x) Evil(x) yields: King(John) Greedy(John) Evil(John) King(Richard) Greedy(Richard) Evil(Richard) King(Father(John) Greedy(Father(John) Evil(Father(John) . . .,4,October 27, 202

3、0,Existential instantiation (EI),For any sentence , variable v, and constant symbol k that does not appear elsewhere in the knowledge base: v Subst(v/k, ) E.g., x Crown(x) OnHead(x,John) yields: Crown(C1) OnHead(C1,John) provided C1 is a new constant symbol, called a Skolem constant,5,October 27, 20

4、20,Existential instantiation contd,UI can be applied several times to add new sentences; the new KB is logically equivalent to the old. EI can be applied once to replace the existential sentence; the new KB is not equivalent to the old but is satisfiable if the old KB was satisfiable.,6,October 27,

5、2020,Reduction to propositional inference,Suppose the KB contains just the following: x King(x) Greedy(x) Evil(x) King(John) Greedy(John) Brother(Richard,John) Instantiating the universal sentence in all possible ways, we have: King(John) Greedy(John) Evil(John) King(Richard) Greedy(Richard) Evil(Ri

6、chard) King(John) Greedy(John) Brother(Richard,John) The new KB is propositionalized: proposition symbols are King(John), Greedy(John), Evil(John), King(Richard), etc.,7,October 27, 2020,Reduction contd.,CLAIM: A ground sentence is entailed by a new KB iff entailed by the original KB. CLAIM: Every F

7、OL KB can be propositionalized so as to preserve entailment IDEA: propositionalize KB and query, apply resolution, return result PROBLEM: with function symbols, there are infinitely many ground terms, e.g., Father(Father(Father(John),8,October 27, 2020,Reduction contd.,THEOREM: Herbrand (1930). If a

8、 sentence is entailed by an FOL KB, it is entailed by a finite subset of the propositionalized KB IDEA: For n = 0 to do create a propositional KB by instantiating with depth-n terms see if is entailed by this KB PROBLEM: works if is entailed, loops if is not entailed THEOREM: Turing (1936), Church (

9、1936) Entailment for FOL is semidecidable algorithms exist that say yes to every entailed sentence, but no algorithm exists that also says no to every nonentailed sentence.,9,October 27, 2020,Problems with propositionalization,Propositionalization seems to generate lots of irrelevant sentences. E.g.

10、, from: x King(x) Greedy(x) Evil(x) King(John) y Greedy(y) Brother(Richard,John) It seems obvious that Evil(John), but propositionalization produces lots of facts such as Greedy(Richard) that are irrelevant. With p k-ary predicates and n constants, there are pnk instantiations!,10,October 27, 2020,U

11、nification,We can get the inference immediately if we can find a substitution such that King(x) and Greedy(x) match King(John) and Greedy(y) = x/John,y/John works Unify( ,) = if = p q Knows(John,x) Knows(John,Jane) Knows(John,x)Knows(y,OJ) Knows(John,x) Knows(y,Mother(y) Knows(John,x)Knows(x,OJ) Sta

12、ndardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ),11,October 27, 2020,Unification,We can get the inference immediately if we can find a substitution such that King(x) and Greedy(x) match King(John) and Greedy(y) = x/John,y/John works Unify( ,) = if = p q Knows(John,x) Knows(John,

13、Jane) x/Jane Knows(John,x)Knows(y,OJ) Knows(John,x) Knows(y,Mother(y) Knows(John,x)Knows(x,OJ) Standardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ),12,October 27, 2020,Unification,We can get the inference immediately if we can find a substitution such that King(x) and Greedy(x) m

14、atch King(John) and Greedy(y) = x/John,y/John works Unify( ,) = if = p q Knows(John,x) Knows(John,Jane) x/Jane Knows(John,x)Knows(y,OJ) x/OJ,y/John Knows(John,x) Knows(y,Mother(y) Knows(John,x)Knows(x,OJ) Standardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ),13,October 27, 2020,Un

15、ification,We can get the inference immediately if we can find a substitution such that King(x) and Greedy(x) match King(John) and Greedy(y) = x/John,y/John works Unify( ,) = if = p q Knows(John,x) Knows(John,Jane) x/Jane Knows(John,x)Knows(y,OJ) x/OJ,y/John Knows(John,x) Knows(y,Mother(y)y/John,x/Mo

16、ther(John) Knows(John,x)Knows(x,OJ) Standardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ),14,October 27, 2020,Unification,We can get the inference immediately if we can find a substitution such that King(x) and Greedy(x) match King(John) and Greedy(y) = x/John,y/John works Unify(

17、,) = if = p q Knows(John,x) Knows(John,Jane) x/Jane Knows(John,x)Knows(y,OJ) x/OJ,y/John Knows(John,x) Knows(y,Mother(y)y/John,x/Mother(John) Knows(John,x)Knows(x,OJ) fail Standardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ),15,October 27, 2020,Unification,To unify Knows(John,x)

18、and Knows(y,z), = y/John, x/z or = y/John, x/John, z/John The first unifier is more general than the second. There is a single most general unifier (MGU) that is unique up to renaming of variables. MGU = y/John, x/z ,16,October 27, 2020,The unification algorithm,17,October 27, 2020,The unification a

19、lgorithm,18,October 27, 2020,The unification algoritm (revisited),This is described for example in John Lloyds book Foundations of Logic Programming. The algorithm unifies a set of literals. A literal is an expression of the form predicate_name(list of terms) where a term is either a constant, a var

20、iable, or of the form functor(list of terms), for example p(X,f(Y,Z) is a literal. A substitution S is a finite set of the form v1/t1,.,vn/tn where the vis are variables and the tis are terms. It means the substitution of those terms for those variables. e S denotes the result of performing the subs

21、titution S on expression e.,19,October 27, 2020,The unification algoritm (revisited),Two substitutions S = u1/s1,.,um/sm and T = v1/t1,.,vn/tn can be composed S T by forming u1/s1 T,.,um/sm T, v1/t1,.,vn/tn and then deleting any ui/si T for which ui=si T , and also deleting any vk/tk for which vk is

22、 a member of u1,.,um Note that substitution is associative but not commutative, so s(tu) = (st)u, but not st = ts. A disagreement set of a set of literals is formed by moving a pointer from the left of each expression until the strings of characters up to that point are not all identical. The set of

23、 terms immediately to the right from that point is the disagreement set. e.g. for the set of literals S = p(f(x),h(y),a), p(f(x),z,a), p(f(x),h(y),b) we have the disagreement set h(y),z.,20,October 27, 2020,The unification algoritm (revisited),The unification algorithm Put k=0 and T0=. If S Tk is un

24、ified, i.e. a singleton, then stop, Tk is the mgu of S. Otherwise form the disagreement set Dk of S Tk . If there exist v and t in Dk such that v is a variable that does not occur in t, then put Tk+1 = Tk v/t, increment k and go to 2. Otherwise stop, S is ununifiable. Example S = p(a,x,h(g(z),p(z,h(

25、y),h(y) T0 = empty. D0 =a,z, T1 = z/a and S T1 =p(a,x,h(g(a),p(a,h(y),h(y) D1 = x,h(y), T2 =z/a,x/h(y) and S T2=p(a,h(y),h(g(a),p(a,h(y),h(y) D2 = y,g(a), T3 =z/a,x/h(g(a),y(g(a) and S T3 =p(a,h(g(a),h(g(a) Thus S is unifiable and T3 is an mgu.,21,October 27, 2020,Generalized Modus Ponens (GMP),p1,

26、p2, , pn, ( p1 p2 pn q) q p1 is King(John) p1 is King(x) p2 is Greedy(y) p2 is Greedy(x) is x/John,y/John q is Evil(x) q is Evil(John) GMP used with KB of definite clauses (exactly one positive literal). All variables assumed universally quantified.,where pi = pi for all i,22,October 27, 2020,Soundn

27、ess of GMP,Need to show that p1, , pn, (p1 pn q) |= q provided that pi = pi for all I LEMMA: For any sentence p, we have p |= p by UI (p1 pn q) |= (p1 pn q) = (p1 pn q) p1, , pn |= p1 pn |= p1 pn From 1 and 2, q follows by ordinary Modus Ponens.,23,October 27, 2020,Example knowledge base,The law say

28、s that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American. Prove that Col. West is a criminal,24,October 27, 2020,Example knowledge base contd.,. it is a

29、crime for an American to sell weapons to hostile nations:,25,October 27, 2020,Example knowledge base contd.,. it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x),26,October 27, 2020,Example knowledge base contd.,. it is a crime

30、for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x) Nono has some missiles,27,October 27, 2020,Example knowledge base contd.,. it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Cri

31、minal(x) Nono has some missiles, i.e., x Owns(Nono,x) Missile(x): Owns(Nono,M1) and Missile(M1),28,October 27, 2020,Example knowledge base contd.,. it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x) Nono has some missiles, i.e.

32、, x Owns(Nono,x) Missile(x): Owns(Nono,M1) and Missile(M1) all of its missiles were sold to it by Colonel West,29,October 27, 2020,Example knowledge base contd.,. it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x) Nono has some

33、 missiles, i.e., x Owns(Nono,x) Missile(x): Owns(Nono,M1) and Missile(M1) all of its missiles were sold to it by Colonel West Missile(x) Owns(Nono,x) Sells(West,x,Nono),30,October 27, 2020,Example knowledge base contd.,. it is a crime for an American to sell weapons to hostile nations: American(x) W

34、eapon(y) Sells(x,y,z) Hostile(z) Criminal(x) Nono has some missiles, i.e., x Owns(Nono,x) Missile(x): Owns(Nono,M1) and Missile(M1) all of its missiles were sold to it by Colonel West Missile(x) Owns(Nono,x) Sells(West,x,Nono) Missiles are weapons:,31,October 27, 2020,Example knowledge base contd.,.

35、 it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x) Nono has some missiles, i.e., x Owns(Nono,x) Missile(x): Owns(Nono,M1) and Missile(M1) all of its missiles were sold to it by Colonel West Missile(x) Owns(Nono,x) Sells(West,x

36、,Nono) Missiles are weapons: Missile(x) Weapon(x),32,October 27, 2020,Example knowledge base contd.,. it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x) Nono has some missiles, i.e., x Owns(Nono,x) Missile(x): Owns(Nono,M1) and

37、 Missile(M1) all of its missiles were sold to it by Colonel West Missile(x) Owns(Nono,x) Sells(West,x,Nono) Missiles are weapons: Missile(x) Weapon(x) An enemy of America counts as hostile“:,33,October 27, 2020,Example knowledge base contd.,. it is a crime for an American to sell weapons to hostile

38、nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x) Nono has some missiles, i.e., x Owns(Nono,x) Missile(x): Owns(Nono,M1) and Missile(M1) all of its missiles were sold to it by Colonel West Missile(x) Owns(Nono,x) Sells(West,x,Nono) Missiles are weapons: Missile(x) Weapon(x) An enemy

39、 of America counts as hostile“: Enemy(x,America) Hostile(x),34,October 27, 2020,Example knowledge base contd.,. it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x) Nono has some missiles, i.e., x Owns(Nono,x) Missile(x): Owns(No

40、no,M1) and Missile(M1) all of its missiles were sold to it by Colonel West Missile(x) Owns(Nono,x) Sells(West,x,Nono) Missiles are weapons: Missile(x) Weapon(x) An enemy of America counts as hostile“: Enemy(x,America) Hostile(x) West, who is American ,35,October 27, 2020,Example knowledge base contd

41、.,. it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x) Nono has some missiles, i.e., x Owns(Nono,x) Missile(x): Owns(Nono,M1) and Missile(M1) all of its missiles were sold to it by Colonel West Missile(x) Owns(Nono,x) Sells(Wes

42、t,x,Nono) Missiles are weapons: Missile(x) Weapon(x) An enemy of America counts as hostile“: Enemy(x,America) Hostile(x) West, who is American American(West),36,October 27, 2020,Example knowledge base contd.,. it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Se

43、lls(x,y,z) Hostile(z) Criminal(x) Nono has some missiles, i.e., x Owns(Nono,x) Missile(x): Owns(Nono,M1) and Missile(M1) all of its missiles were sold to it by Colonel West Missile(x) Owns(Nono,x) Sells(West,x,Nono) Missiles are weapons: Missile(x) Weapon(x) An enemy of America counts as hostile“: E

44、nemy(x,America) Hostile(x) West, who is American American(West) The country Nono, an enemy of America ,37,October 27, 2020,Example knowledge base contd.,. it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x) Nono has some missile

45、s, i.e., x Owns(Nono,x) Missile(x): Owns(Nono,M1) and Missile(M1) all of its missiles were sold to it by Colonel West Missile(x) Owns(Nono,x) Sells(West,x,Nono) Missiles are weapons: Missile(x) Weapon(x) An enemy of America counts as hostile“: Enemy(x,America) Hostile(x) West, who is American Americ

46、an(West) The country Nono, an enemy of America Enemy(Nono,America),38,October 27, 2020,Forward chaining algorithm,39,October 27, 2020,Forward chaining proof,40,October 27, 2020,Forward chaining proof,41,October 27, 2020,Forward chaining proof,42,October 27, 2020,Properties of forward chaining,Sound

47、and complete for first-order definite clauses. Cfr. Propositional logic proof. Datalog = first-order definite clauses + no functions (e.g. crime KB) FC terminates for Datalog in finite number of iterations May not terminate in general definite clauses with functions if is not entailed This is unavoi

48、dable: entailment with definite clauses is semidecidable,43,October 27, 2020,Efficiency of forward chaining,Incremental forward chaining: no need to match a rule on iteration k if a premise wasnt added on iteration k-1 match each rule whose premise contains a newly added positive literal. Matching i

49、tself can be expensive: Database indexing allows O(1) retrieval of known facts e.g., query Missile(x) retrieves Missile(M1) Matching conjunctive premises against known facts is NP-hard. Forward chaining is widely used in deductive databases,44,October 27, 2020,Hard matching example,Colorable() is in

50、ferred iff the CSP has a solution CSPs include 3SAT as a special case, hence matching is NP-hard,Diff(wa,nt) Diff(wa,sa) Diff(nt,q) Diff(nt,sa) Diff(q,nsw) Diff(q,sa) Diff(nsw,v) Diff(nsw,sa) Diff(v,sa) Colorable() Diff(Red,Blue) Diff (Red,Green) Diff(Green,Red) Diff(Green,Blue) Diff(Blue,Red) Diff(

51、Blue,Green),45,October 27, 2020,Backward chaining algorithm,SUBST(COMPOSE(1, 2), p) = SUBST(2, SUBST(1, p),46,October 27, 2020,Backward chaining example,47,October 27, 2020,Backward chaining example,48,October 27, 2020,Backward chaining example,49,October 27, 2020,Backward chaining example,50,Octobe

52、r 27, 2020,Backward chaining example,51,October 27, 2020,Backward chaining example,52,October 27, 2020,Backward chaining example,53,October 27, 2020,Backward chaining example,54,October 27, 2020,Properties of backward chaining,Depth-first recursive proof search: space is linear in size of proof. Inc

53、omplete due to infinite loops fix by checking current goal against every goal on stack Inefficient due to repeated subgoals (both success and failure) fix using caching of previous results (extra space!) Widely used for logic programming,55,October 27, 2020,Logic programming,Logic programming Identi

54、fy problem Assemble information Encode info in KB Encode problem instances as facts Ask queries Find false facts.,Procedural programming Identify problem Assemble information Figure out solution Program solution Encode problem instance as data Apply program to data Debug procedural errors,Should be

55、easier to debug Capital(NY, US) than x=x+2,56,October 27, 2020,Logic programming: Prolog,BASIS: backward chaining with Horn clauses + bells complete for FOL,59,October 27, 2020,Conversion to CNF,Everyone who loves all animals is loved by someone: x y Animal(y) Loves(x,y) y Loves(y,x) Eliminate bicon

56、ditionals and implications x y Animal(y) Loves(x,y) y Loves(y,x) Move inwards: x p x p, x p x p x y (Animal(y) Loves(x,y) y Loves(y,x) x y Animal(y) Loves(x,y) y Loves(y,x) x y Animal(y) Loves(x,y) y Loves(y,x),60,October 27, 2020,Conversion to CNF contd.,Standardize variables: each quantifier shoul

57、d use a different one: x y Animal(y) Loves(x,y) z Loves(z,x) Skolemize: a more general form of existential instantiation.Each existential variable is replaced by a Skolem function of the enclosing universally quantified variables: x Animal(F(x) Loves(x,F(x) Loves(G(x),x) Drop universal quantifiers: Animal(F(x) Loves(x,F(x) Loves(G(x),x)