ch9-一阶逻辑中的推理-----人工智能课程---北大计算机研究所.ppt

,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,第九章、一阶逻辑中的推理,命题与一阶推理,量词的实例化（,和,）,如何将一阶推理简化为命题推理（命题化）,合一与提升,构造直接用于一阶语句的推理规则,前向链接,反向链接,Universal 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,(,Richard,),King,(,Father,(,John,),Greedy,(,Father,(,John,),Evil,(,Father,(,John,),.,.,.,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,(,C,1,),OnHead,(,C,1,John,),provided,C,1,is a new constant symbol,called a,Skolem constant,Reduction contd.,Every FOL KB can be propositionalized so as to preserve entailment,（,中文书翻译不准确！,）,(A ground sentence is entailed 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,),Reduction contd.,Theorem:Herbrand(1930).If a 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(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.),Problems with,propositionalization,Propositionalization seems to generate lots of irrelevant sentences.,E.g.,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,p,n,k,instantiations.,第九章、一阶逻辑中的推理,命题与一阶推理,量词的实例化（,和,）,如何将一阶推理简化为命题推理（命题化）,合一与提升,构造直接用于一阶语句的推理规则,前向链接,反向链接,归结,Generalized Modus Ponens,p,1,p,2,p,n,(p,1,p,2,p,n,q),subst(q,),p,1,is,King,(,John,)p,1,is,King,(,x,),p,2,is,Greedy,(,y,)p,2,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 quantified,GMP is called a lifted version of Modus Ponens,where subst(p,i,)=subst(p,i,)for all,i,Unification,Lifted inference rules require finding substitutions that make different logical expressions look identical.This process is called unification.,Unify(,)=,if subst(,)=subst(,),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(z,17,OJ),Algorithm for finding MGU,在复合表达式如,F(A,B),中，函数,OP,提取函数符,F,，,ARGS,提取参数表,(A,B),。,Algorithm(contd),OCCUR-CHECK,：当将一个变量和一个复合过程进行匹配时，必须检查该变量是否,在该项中出现。,第九章、一阶逻辑中的推理,命题与一阶推理,量词的实例化（,和,）,如何将一阶推理简化为命题推理（命题化）,合一与提升,构造直接用于一阶语句的推理规则,前向链接,反向链接,归结,Example 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 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,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,M,1,)and Missile(M,1,),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,American(West),The country Nono,an enemy of America,Enemy(Nono,America),Forward chaining proof,Forward chaining proof,Properties 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 clauses is semidecidable,前向链接算法中可能的复杂性来源,算法的“内循环”涉及寻找所有可能的合一者，把规则的前提与知识库中一个适合的事实集进行合一（模式匹配），成本可能很高。,算法每次遍历都要对每条规则进行重新检查，即使每次遍历添加到知识库的规则很少。,算法可能生成许多与目标无关的事实,模式匹配和约束满足之间的联系,Colorable,()is inferred 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(Blue,Green),增量前向链接,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,无关的事实：解决办法,采用反向链接,把前向链接限制在一个选定的规则子集内,在演绎数据库内，利用从目标得到的信息重写规则集，从而在向前推理过程中只考虑相关的变量绑定。（魔法集方法，介于前向推理和反向预处理之间）,Backward chaining algorithm,SUBST(COMPOSE(,1,2,),p)=SUBST(,2,SUBST(,1,p),Backward chaining example,Backward chaining example,Backward chaining example,Backward chaining example,Backward chaining example,Backward chaining example,Backward chaining example,Properties of backward chaining,Depth-first recursive proof search:space is linear 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 programming,Logic programming:Prolog,Algorithm=Logic+Control,Basis:backward chaining with Horn clauses+bells&whistles,Widely used in Europe,Japan(basis of 5th Generation project),Compilation techniques,60 million LIPS,Program=set of clauses=,head:-literal,1,literal,n,.,criminal(X):-american(X),weapon(Y),sells(X,Y,Z),hostile(Z).,Depth-first,left-to-right backward chaining,Built-in predicates for arithmetic etc.,e.g.,X is Y*Z+3,Built-in predicates that have side effects(e.g.,input and output predicates,assert/retract predicates),Closed-world assumption(negation as failure),e.g.,given,alive(X):-not dead(X).,alive(joe),succeeds if,dead(joe),fails,Prolog,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=1,2,A=1 B=2,A=1,2 B=,小结,一阶逻辑的命题化，运行速度很慢，产生大量和目标无关的句子。,合一消除了一阶逻辑证明的实例化步骤，从而提高了推理过程的效率。,GMP,利用合一提供了一条自然而又强大的推理规则。,GMP,对于确定字句是完备的，但蕴涵问题是半可判定的。,前向链接用于演绎数据库和产生式系统中,逻辑程序设计系统，如,Prolog,中采用了反向链接,HW,9.6,9.9,9.10,9.11,