人工智能谓词逻辑与归结原理

,人工智能谓词逻辑与归结原理,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,*,人工智能谓词逻辑与归结原理,人工智能谓词逻辑与归结原理,合取范式：仅由有限个简单析取式构成的合取式，,即合取项是单元子句或单元子句的析取,形如：PPQPQ,求合取范式的根本原那么：,利用“对“的分配,求合取范式的根本步骤：,削去对于 ， ， 来说冗余的联结词,内移或削去否认号,利用分配律,2,人工智能谓词逻辑与归结原理,求取,p,(,q,r),s,的合取范式,=(,p, (,q,r),s,=,p,(,q,r),s,=,p,(,q, ,r),s,=,p,(q, ,r),s,=,p,s,(q, ,r),=p s q p s r),p,(,q,r),s,3,人工智能谓词逻辑与归结原理,我们说如果有条件F1，F2，F3.Fn同时成立，那么有结论B成立。,F1 F2 F3 Fn B 永假,(,(F1,F2,F3,Fn),B ),不成立, (F1 F2 F3 Fn) B成立永真,可以表示说：,F1 F2 F3 Fn B成立永真,4,根底知识,谓词公式、某些推理规那么以及置换合一等概念。,子句，由文字的析取组成的公式；,一个原子公式和原子公式的否认都叫做文字。,消解 当消解可使用时，消解过程被应用于母体子句对，以便产生一个导出子句。,例如，如果存在某个公理 E1E2 和另一公理E2E3 ，那么 E1E3在逻辑上成立。这就是消解，而称E1E3为E1E2和E2E3的消解式resolvent 。,任一谓词演算公式可以化成一个子句集,子句集的求取,人工智能谓词逻辑与归结原理,5,人工智能谓词逻辑与归结原理,(1)消去蕴涵符号,只应用和符号，以AB替换A=B。,(2)减少否认符号的辖域,每个否认符号最多只用到一个谓词符号上，并反复应用狄摩根定律。,例如： 以AB代替(AB),以AB代替(AB),以( x)A代替( x)A,以( x)A代替( x)A,以A代替(A),(3)对变量标准化,6,人工智能谓词逻辑与归结原理,在任一量词辖域内，受该量词约束的变量为一哑元(虚构变量)，它可以在该,辖域内处处统一地被另一个没有出现过的任意变量所代替，而不改变公式的,真值。适宜公式中变量的标准化，意味着对哑元改名以保证每个量词有其自,己唯一的哑元。例如，把,标准化而得到:,(4)消去存在量词,对于一个受存在量词约束的变量，如果它不受全称量词约束，那么该变量用一,个常量来代替，如果它受全称量词约束，那么该变量用一个含有全称量词对应,变量的函数Skolem函数来代替。,Skolem函数所使用的函数符号必须是新的，即不允许是公式中已经出现过的,函数符号。,替代的常量符号必须是个新的常量符号，它未曾在公式中其它地方使用过。,7,人工智能谓词逻辑与归结原理,例如：,(5)化为前束形到这一步，已不留下任何存在量词，而且每个全称量词都有自己的变量。把所有全称量词移到公式的左边，并使每个量词的辖域包括这个量词后面公式的整个局部。所得公式称为前束形。前束形公式由前缀和母式组成，前缀由全称量词串组成，母式由没有量词的公式组成，即 前束形 = (前缀) (母 式) 全称量词串 无量词公式,8,人工智能谓词逻辑与归结原理,(6)把母式化为合取范式,任何母式都可写成由一些谓词公式和(或)谓词公式的否认的析取的有限集组,成的合取。这种母式叫做合取范式。我们可以反复应用分配律。把任一母式,化成合取范式。例如，我们把,(7)消去全称量词,到了这一步，所有余下的量词均被全称量词量化了。同时，全称量词的次序,也不重要了。因此，我们可以消去前缀，即消去明显出现的全称量词。,(8)消去连词符号,用(AB),(AC)代替(AB)(AC)，以消去明显的符号。反复代替的,结果，最后得到一个有限集，其中每个公式是文字的析取。任一个只由文字,的析取构成的适宜公式叫做一个子句。,9,人工智能谓词逻辑与归结原理,(9),更换变量名称,可以更换变量符号的名称，使一个变量符号不出现在一个以上的子句中。,例如，对于子集,P(x),P(y)Pf(x,y),P(x)Qx,g(x),P(x),Pg(x),，,在更改变量名后，可以得到子句集：,P(,x1,),P(y)Pf(,x1,y),P(,x2,)Q,x2,g(,x2,),P(,x3,),Pg(,x3,) ,10,人工智能谓词逻辑与归结原理,例：,( x)P(x)( y)P(y) P(f(x,y) ( y)Q(x,y)P(y),( x)P(x)( y)P(y) P(f(x,y) ( y)Q(x,y)P(y),( x)P(x)( y)P(y) P(f(x,y) ( y)Q(x,y) P(y),( x)P(x)( y)P(y) P(f(x,y) ( w)Q(x,w) P(w),( x)P(x)( y)P(y) P(f(x,y) Q(x,g(x) P(g(x),( x) ( y) P(x) P(y) P(f(x,y) Q(x,g(x) P(g(x),11,人工智能谓词逻辑与归结原理,( x) ( y) P(x)P(y) P(f(x,y) P(x) Q(x,g(x),P(x) P(g(x), P(x)P(y) P(f(x,y) P(x) Q(x,g(x)P(x)P(g(x), P(x)P(y) P(f(x,y),P(x) Q(x,g(x),P(x)P(g(x), P(x1)P(y) P(f(x1,y),P(x2) Q(x2,g(x2),P(x3)P(g(x3),12,人工智能谓词逻辑与归结原理,令L1为任一原子公式，L2为另一原子公式； L1和L2具有一样的谓词符号，但一般具有不同的变量。,两子句L1和L2如果L1和L2具有最一般合一者，那么通过消解可以从这两个父辈子句推导出一个新子句()。这个新子句叫做消解式。它是由取这两个子句的析取，然后消去互补对而得到的。,13,人工智能谓词逻辑与归结原理,(a),假言推理,(b),合并,(c),重言式,(d),链式,(,三段论,),(e),空子句,(,矛盾,),消解可以合并几个运算为一简单的推理规那么,14,人工智能谓词逻辑与归结原理,例,1,例,2,例,3,15,人工智能谓词逻辑与归结原理,16,人工智能谓词逻辑与归结原理,根本思想 把要解决的问题作为一个要证明的命题，其目标公式被否认并化成子句形，然后添加到命题公式集中去,把消解反演系统应用于联合集，并推导出一个空子句(NIL)，产生一个矛盾，这说明目标公式的否认式不成立，即有目标公式成立，定理得证，问题得到解决。这与数学中反证法的思想十分相似。,17,人工智能谓词逻辑与归结原理,消解反演,反演求解的步骤,给出一个公式集S和目标公式L，通过反证或反演来求证目标公式L，其证明步骤如下： (1)否认L，得L；(2)把L添加到S中去；(3)把新产生的集合L，S化成子句集；(4)应用消解原理，力图推导出一个表示矛盾的空子句NIL。,18,人工智能谓词逻辑与归结原理,消解反演,反演求解的正确性,设公式,L,在逻辑上遵循公式集,S,，那么按照定义满足,S,的每个解释也满足,L,。决不会有满足,S,的解释能够满足,L,的，所以不存在能够满足并集,S,L,的解释。如果一个公式集不能被任一解释所满足，那么这个公式是不可满足的。因此，如果,L,在逻辑上遵循,S,，那么,S,L,是不可满足的。可以证明，如果消解反演反复应用到不可满足的子句集，那么最终将要产生空子句,NIL,。因此，如果,L,在逻辑上遵循,S,，那么由并集,S,L,消解得到的子句，最后将产生空子句；反之，可以证明，如果从,S,L,的子句消解得到空子句，那么,L,在逻辑上遵循,S,。,19,人工智能谓词逻辑与归结原理,例,:,假设任何通过计算机考试并获奖的人是快乐的,任何肯学习或幸运的人都可以通过所有的考试,张不肯学习但他是幸运的,任何幸运的人都能获奖,.,求证,:,张是快乐的,.,20,人工智能谓词逻辑与归结原理,1.( x)(pass(x,computer)win(x,prize) happy(x),2.( x)( y)(study(x)lucky(x) pass(x,y),3. study(zhang)lucky(zhang),4.( x)(Lucky(x) win(x,prize),5. happy(zhang),21,人工智能谓词逻辑与归结原理, pass(x,computer) win(x,prize)happy(x), study(y)pass(y,z), lucky(u)pass(u,v), study(zhang),lucky(zhang), lucky(w) win(w,prize),happy(zhang),22,人工智能谓词逻辑与归结原理,23,人工智能谓词逻辑与归结原理,反演求解过程,从反演树求取答案步骤,把由目标公式的否认产生的每个子句添加到目标公式否认之否认(肯定永真式)的子句中去。,按照反演树，执行和以前一样的消解，直至在根部得到某个子句止。,用根部的子句作为一个答复语句。,实质,把一棵根部有NIL的反演树变换为根部带有答复语句的一棵证明树。,24,人工智能谓词逻辑与归结原理,If Fido goes wherever John goes and if John is at school， where is Fido?,先把问题用谓词逻辑公式表示：,前提公式集：,(x)ATJohn，xATFido，x,ATJohn，School,目标公式： (x) ATFido，x,25,人工智能谓词逻辑与归结原理,菲多在哪里,例题的反演树,从消解求取答案例题的反演树,修改证明树,26,人工智能谓词逻辑与归结原理,菲多在哪里,例题的修改证明树,27,人工智能谓词逻辑与归结原理,：会朗读的人是识字的；,海豚都不识字；,有些海豚是很机灵的。,证明：有些很机灵的东西不会朗读。,把问题用谓词逻辑描述如下：,： xRxLx, xDxLx, xDxIx,求证： xIxRx,28,人工智能谓词逻辑与归结原理,例：,寒冷户外戴帽子。,cold,outdoor,wearing,应届高中生，得过数学或物理竞赛的一,等奖，保送上北京大学。,p,( r,t ),q,29,人工智能谓词逻辑与归结原理,定义,基于规那么的问题求解系统运用IfThen规那么来建立，每个if可能与某断言(assertion)集中的一个或多个断言匹配。有时把该断言集称为工作内存，then局部用于规定放入工作内存的新断言。这种基于规那么的系统叫做规那么演绎系统。在这种系统中，通常称每个if局部为前项，称每个then局部为后项。,30,人工智能谓词逻辑与归结原理,定义,正向规那么演绎系统是从事实到目标进展操作的，即从状况条件到动作进展推理的，也就是从if到then的方向进展推理的,求解过程,事实表达式的与或形变换,在基于规那么的正向演绎系统中，我们把事实表示为非,蕴涵形式的与或形，作为系统的总数据库。,事实表达式的与或图表示,31,人工智能谓词逻辑与归结原理,32,人工智能谓词逻辑与归结原理,我们把允许用作规那么的公式类型限制为以下形式： L W,式中：L是单文字；,W为与或形的唯一公式。,33,人工智能谓词逻辑与归结原理,单文字前项的任何蕴涵式，不管其量化情况如何都可以化为某种量化辖域为整个蕴涵式的形式。,34,人工智能谓词逻辑与归结原理,不含变量的与或图,应用一条 规那么得到的与或图,PQS, RS, PQTU, RTU,(1)XZPQ ,YZPQ , (2)RXZ ,RYZ,规那么S (X Y) Z,35,人工智能谓词逻辑与归结原理,36,人工智能谓词逻辑与归结原理,定义,逆向规那么演绎系统是从then向if进展推理的，即从目标或动作向事实或状况条件进展推理的。,求解过程,目标表达式的与或形式,与或图的B规那么变换,作为终止条件的事实节点的一致解图,37,人工智能谓词逻辑与归结原理,概念,正向和逆向组合系统是建立在两个系统相结合的根底上的。此组合系统的总数据库由表示目标和表示事实的两个与或图构造组成。这些与或图构造分别用正向系统的F规那么和逆向系统的B规那么来修正。,38,汇报结束,谢谢大家,!,请各位批评指正,