1、智能计算研究中心IX. Inference in First-order logic Autumn 2012Instructor: Wang XiaolongHarbin Institute of Technology, Shenzhen Graduate SchoolIntelligent Computation Research Center(HITSGS)2Outline Reducing first-order inference to propositional inference Unification Generalized Modus Ponens Forward chaini
2、ng Backward chaining Resolution3Universal instantiation (UI) Every instantiation of a universally 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(Ric
3、hard)King(Father(John) Greedy(Father(John) Evil(Father(John)4Existential 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 co
4、nstant symbol, called a Skolem constant5Reduction to propositional inferenceSuppose 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(Richa
5、rd) Greedy(Richard) Evil(Richard)King(John)Greedy(John)Brother(Richard,John)The new KB is propositionalized: proposition symbols are King(John), Greedy(John), Evil(John), King(Richard), etc.6Reduction contd. Every FOL KB can be propositionalized so as to preserve entailment (A ground sentence is ent
6、ailed by new KB iff entailed by original KB) 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)7Reduction contd.Theorem: Herbrand (1930). If a sentence is entailed by an FOL KB,
7、 it is entailed by a finite subset of the propositionalized KBIdea: For n = 0 to do create a propositional KB by instantiating with depth (n) terms see if is entailed by this KBProblem: works if is entailed, loops if is not entailedTheorem: Turing (1936), Church (1936) Entailment for FOL is semideci
8、dable (algorithms exist that say yes to every entailed sentence, but no algorithm exists that also says no to every nonentailed sentence.)8Problems with propositionalization Propositionalization seems to generate lots of irrelevant sentences. E.g., from:x King(x) Greedy(x) Evil(x)King(John)y Greedy(
9、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.9UnificationWe can get the inference immediately if we can find a substitution s
10、uch that King(x) and Greedy(x) match King(John) and Greedy(y) = x/John,y/John worksUnify(p , q) = if Subst (, p) = Subst (, q) 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) 10UnificationWe can get the inference immediately if we c
11、an find a substitution such that King(x) and Greedy(x) match King(John) and Greedy(y) = x/John,y/John worksUnify(p , q) = if Subst (, p) = Subst (, q) p q Knows(John,x) Knows(John,Jane) x/JaneKnows(John,x)Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)Knows(John,x)Knows(x,OJ) 11UnificationWe can get the
12、 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 worksUnify(p , q) = if Subst (, p) = Subst (, q) p q Knows(John,x) Knows(John,Jane) x/JaneKnows(John,x)Knows(y,OJ) x/OJ,y/JohnKnows(John,x) Knows(y,Mother(y)Knows(John,
13、x)Knows(x,OJ) 12UnificationWe 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 worksUnify(p , q) = if Subst (, p) = Subst (, q) p q Knows(John,x) Knows(John,Jane) x/JaneKnows(John,x)Knows(y,OJ) x/OJ,y/JohnK
14、nows(John,x) Knows(y,Mother(y) y/John,x/Mother(John)Knows(John,x)Knows(x,OJ) 13UnificationWe 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 worksUnify(p , q) = if Subst (, p) = Subst (, q) p q Knows(John,
15、x) Knows(John,Jane) x/JaneKnows(John,x)Knows(y,OJ) x/OJ,y/JohnKnows(John,x) Knows(y,Mother(y)y/John,x/Mother(John)Knows(John,x)Knows(x,OJ) failStandardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ)14Unification To unify Knows(John,x) and Knows(y,z), = y/John, x/z or = y/John, x/Joh
16、n, 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 15The unification algorithm16The unification algorithm17Generalized Modus Ponens (GMP)p1, p2, , pn, ( p1 p2 pn q) Subst (,q)p1 is Kin
17、g(John) p1 is King(x) p2 is Greedy(y) p2 is Greedy(x) is x/John,y/John q is Evil(x) Subst (,q) is Evil(John) GMP used with KB of definite clauses (exactly one positive literal) All variables assumed universally quantifiedwhere Subst ( ,pi) = Subst ( ,pi) for all i18Soundness of GMPNeed to show that
18、p1, , pn, (p1 pn q) Subst (,q) provided that Subst ( ,pi) = Subst ( ,pi) for all iLemma: For any sentence p, we have p Subst (,q) by UI1.(p1 pn q) Subst(,(p1 pn q) = (Subst( ,p1) Subst( ,pn) Subst( ,q)2. p1, , pn p1 pn Subst(,p1) Subst(,pn) 3. From 1 and 2, Subst( ,q) follows by ordinary Modus Ponen
19、s19FOL definite clausesDisjunctions of literals of which exactly one is positive.A definite clause either is atomic or is an implication whose antecedent is a conjunction of positive literals and whose consequent is a single positive literal.Eg.King(x) Greedy(x) Evil(x) King(John) Greedy(y)Unlike pr
20、opositional literals, FOL literals can include variables (universally quantified).Not every KB can be converted into a set of definite clauses. But many can.20Example knowledge base The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of Amer
21、ica, 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.21Example 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
22、 missiles, i.e., x Owns(Nono,x) Missile(x):Owns(Nono,M1) Missile(M1) all of its missiles were sold to it by Colonel WestMissile(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 American(
23、West)The country Nono, an enemy of America Enemy(Nono,America)22Forward chaining algorithm23Forward chaining proof24Forward chaining proofMissile(x) Weapon(x)Missile(x) Owns(Nono,x) Sells(West,x,Nono)Enemy(x,America) Hostile(x)25Forward chaining proofAmerican(x) Weapon(y) Sells(x,y,z) Hostile(z) Cri
24、minal(x)26Properties of forward chaining Sound and complete for first-order definite clauses Datalog = first-order definite clauses + no functions FC terminates for Datalog in finite number of iterations May not terminate in general if is not entailed This is unavoidable: entailment with definite cl
25、auses is semidecidable27Efficiency of forward chainingIncremental 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 literalForward chaining is widely used in deductive databases28Hard match
26、ing exampleColorable() is inferred iff the CSP has a solutionCSPs include 3SAT as a special case, hence matching is NP-hardNote: Reference to: John E. Hopcroft, Rajeev Motwani, Jefferey D. Ullman, “Introduction to automata theory, language, and computation” (2nd), Tsinghua university press, Addison-
27、Wesley.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(Blue,Green)29 Examples of long distance restriction30 In the w-n-gram model, finding charac
28、ter or words corresponding to the speech syllable input yi(一,疑,以,已,衣,亿,依,易,医,.)zhi(只,之,直,知,制,指,纸,支,芝,.)piaoliangde(漂亮的)xiao(小,笑,消,削,销,萧,效,宵,晓,.)hua(话,花,化,画,华,划,滑,哗,猾,.)mao(毛,冒,帽,猫,矛,卯,貌,茂,贸,.).31 and the relevant rules 花 plant 猫 animal 一 number 小 adj 漂亮的 adj 花 adj adj + animal animal adj + plant pla
29、nt number+ 只+animal animal number+ 枝+plant plant.32 A good example of recursive nature is number. A group of simplified rules for describing Chinese number are given below: MX=一，二，三，四，五，六，七，八，九MX0=零MW=十,百,千,万,亿,兆MWW=万,亿,兆MH=好些, 许多, 若干, 几, 两MX-MX0(r1)MX0+MX0-MMX(r2)MX0+MMX-MMX(r3)MX+MW+MX-MX(r4)MX+MW
30、+零+MX-MX(r5)MW+MWW-MW(r6)MWW-MW(r7)MX+MW-M (r8)33 十+MX-MS (r9)MS+MWW-M(r10)MS+MWW+MX-MX(r11)MX0+点+MX-M (r12)MX0+点+MMX-M(r13)MS+点+MX-M (r14)MS+点+MMX-M (r15)M+倍-MB(r16)MX0-M(r17)MMX-M(r18)MW-M(r19)MB-M(r20)MH-M(r21)MS-M(r22)34Backward chaining algorithm SUBST(COMPOSE(1, 2), p) = SUBST(2, SUBST(1, p)35
31、Backward chaining example36Backward chaining example37Backward chaining example38Backward chaining example39Backward chaining example40Backward chaining example41Backward chaining example42Backward chaining example43Properties of backward chaining Depth-first recursive proof search: space is linear
32、in size of proof Incomplete 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 programming44Logic programming: PrologAlgorithm = Logic
33、 + ControlProgram = set of clauses = head :- literal1, literaln.criminal(X) :- american(X), weapon(Y), sells(X,Y,Z), hostile(Z).Depth-first, left-to-right backward chainingA set of built-in functions for arithmetic etc., e.g., X is Y*Z+3Built-in predicates that have side effects (e.g., input and out
34、put predicates, assert/retract predicates)Closed-world assumption (negation as failure) e.g., given alive(X) :- not dead(X). alive(joe) succeeds if dead(joe) fails45Prolog Appending two lists to produce a third:append(,Y,Y). append(X|L,Y,X|Z) :- append(L,Y,Z). query: append(A,B,1,2) ? answers: A= B=
35、1,2 A=1 B=2 A=1,2 B=46Resolution: brief summaryFull first-order version:l1 lk, m1 mnSubst(, l1 li-1 li+1 lk m1 mj-1 mj+1 mn)where Unify(li, mj) = .The two clauses are assumed to be standardized apart so that they share no variables.For example,Rich(x) Unhappy(x) Rich(Ken)Unhappy(Ken)with = x/KenAppl
36、y resolution steps to CNF(KB ); complete for FOL47Conversion to CNF Everyone who loves all animals is loved by someone:x y Animal(y) Loves(x,y) y Loves(y,x) 1. Eliminate biconditionals and implicationsx y Animal(y) Loves(x,y) y Loves(y,x) 2. Move inwards: x p x p, x p x px y (Animal(y) Loves(x,y) y
37、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) 48Conversion to CNF contd.3.Standardize variables: each quantifier should use a different onex y Animal(y) Loves(x,y) z Loves(z,x) 4.Skolemize: a more general form of existential instantiation.Each existential var
38、iable is replaced by a Skolem function of the enclosing universally quantified variables: x Animal(F(x) Loves(x,F(x) Loves(G(x),x)5.Drop universal quantifiers: Animal(F(x) Loves(x,F(x) Loves(G(x),x)6.Distribute over : Animal(F(x) Loves(G(x),x) Loves(x,F(x) Loves(G(x),x)49Resolution proof: definite c
39、lauses50Resolution proof example 2 The problem is:Everyone who loves all animals is loved by someone.Anyone who kills an animal is loved by no one.Jack loves all animals.Either Jack or Curiosity killed the cat, who is named Tuna.Did Curiosity kill the cat?51Resolution proof example 2 contd. First, w
40、e express the original sentences, some background knowledge, and the negated goal G in FOL:A.x y Animal(y) Loves(x,y) y Loves(y,x)B.x y Animal(y) kills(x,y) z Loves(z,x)C.x Animal(x) Loves(Jack,x)D.kills(Jack,Tuna) kills(Curiosity,Tuna)E.Cat(Tuna)F.x Cat(x) Animal(x)G. kills(Curiosity,Tuna)52Resolut
41、ion proof example 2 contd. Second, convert each sentence to CNFA1.Animal(F(x) Loves(G(x),x)A2.Loves(x,F(x) Loves(G(x),x)B. Animal(y) kills(x,y) Loves(z,x)C. Animal(x) Loves(Jack,x)D.kills(Jack,Tuna) kills(Curiosity,Tuna)E.Cat(Tuna)F. Cat(x) Animal(x)G. kills(Curiosity,Tuna)53Resolution proof example 2 contd. The resolution proof that Curiosity killed the cat is given below.54Assignments Ex 9.11
