第二章归结推理方法课前指导2.1归结原理概述2.2命题逻辑的归结2.3谓词逻辑归结法基础2.4归结原理2.5归结过程控制策略2.6Herbrand定理章节小结课前指导【学习目标】本章主要讨论命题逻辑和一元谓词逻辑的归结推理方法。同学需要在熟练掌握一般逻辑知识的基础上,学习Skolem标准形和Herbrand定理,从而对归结原理有一个比较透彻的了解。【学习指南】在学习新知识的同时回顾以前所学的一般逻辑知识。对所涉及的概念和方法不要死记硬背,对于比较抽象的概念,可以通过比较简单的例子来理解。【难重点】应该熟练掌握把逻辑公式的合取范式、Skolem标准形的转化方法、归结法进行归结的过程,掌握线性归结、支撑集归结等归结策略。【知识点】◇归结方法的特点、与其它推理方法的比较◇命题逻辑基础,前束范式,约束变量换名规则◇Skolem标准形的定义,子句和子句集,定理的内容及推广◇H域、H解释、语义树◇合一和置换,归结过程◇归结法的控制策略的原则及基本方法。归结推理知识结构2.1归结原理概述归结原理由J.A.Robinson于1965年提出,又称为消解原理。该原理是Robinson在Herbrand理论基础上提出的一种基于逻辑的、采用反证法的推理方法。由于其理论上的完备性,归结原理成为机器定理证明的主要方法。注意:本课程只讨论一阶谓词逻辑描述下的归结推理方法,不涉及高阶谓词逻辑问题本章首先介绍命题逻辑的归结,并以此为基础介绍谓词逻辑的归结过程及相关的思想、概念和定义,最后给出谓词逻辑归结的基础Herbrand定理的一般形式。定理证明的实质与困难从某种意义上讲大部分人工智能问题都可以转化为一个定理证明问题。定理证明的实质:就是要对给出的(已知的)前提和结论,证明此前提推导出该结论这一事实是永恒的真理。这是非常困难的,几乎是不可实现的。困难所在:要证明在一个论域上一个事件是永真的,就要证明在该域中的每一个点上该事实都成立。很显然,论域是不可数时,该问题不可能解决。即使可数,如果该轮域是无限的,问题也无法简单地解决。Herbrand采用了反证法的思想,将永真性的证明问题转化成为不可满足性的证明问题。Herbrand理论为自动定理证明奠定了理论基础,而Robinson的归结原理使得自动定理证明得以实现。因此,归结推理方法在人工智能推理方法中有着很重要的历史地位。归结法的特点与演绎法完全不同,归结法是一种新的逻辑演算算法。它是一阶逻辑中,至今为止的最有效的半可判定的算法。也是最适合计算机进行推理的逻辑演算方法。半可判定,即,一阶逻辑中任意恒真公式,使用归结原理,总可以在有限步内给以判定(证明其为永真式)。归结法基本原理归结法的基本原理:是采用反证法或者称为反演推理方法,将待证明的表达式(定理)转换成为逻辑公式(谓词公式),然后再进行归结,归结能够顺利完成,则证明原公式(定理)是正确性的。例如:由命题逻辑描述的命题:A1、A2、A3和B,要求证明:如果A1ΛA2ΛA3成立,则B成立,即:A1ΛA2ΛA3→B是重言式(永真式)。归结法的思路:A1ΛA2ΛA3→B是重言式等价于A1ΛA2ΛA3Λ~B是矛盾式,也就是说永假式。反证法:证明A1ΛA2ΛA3Λ~B是矛盾式(永假式)归结的目的:建立基本规则证明该条定理(事实)成立。归结法和其它推理方法的比较语义网络、框架表示、产生式规则等知识表示方法的推理都是以逻辑推理方法为前提的。即,有了规则和已知条件,就能够依据一定的规则和公理顺藤摸瓜找到结果。而归结方法是计算机自动推理、自动推导证明用的推理方法。(同样的内容可以在“数学定理机器证明”中找到。)2.2命题逻辑的归结2.2.1命题逻辑基础逻辑可分为经典逻辑和非经典逻辑经典逻辑包括命题逻辑和谓词逻辑。归结原理是一种主要基于谓词(逻辑)知识表示的推理方法,而命题逻辑是谓词逻辑的基础。因此,在讨论谓词逻辑之前,先讨论命题逻辑的归结,便于内容上的理解。本节中,将主要介绍命题逻辑的归结方法,以及有关的一些基础知识和重要概念,如数理逻辑基本公式变形、前束范式、子句集等。命题例子命题:非真即假的简单陈述句。简单陈述句描述事实、事物的状态、关系等性质。例如:1、1+1=2.2、雪是黑色的。3、北京是中国的首都。4、到冥王星去度假。判断一个句子是否是命题,首先要看它是否是陈述句,而后看它的真值是否唯一。以上的例子都是陈述句,第4句的真值现在是假,随着人类科学的发展,有可能变成真。但不管怎样,真值是唯一的。因此以上例子都是命题。而例如:1、快点走吧!2、到哪去?3、X+Y10等等句子,都不是命题。命题表示公式(1)如何将陈述句转化成命题公式?例如:设“下雨”为p,“骑车上班”为q,1、“只要不下雨,我骑自行车上班”。p是q的充分条件,因而,可得命题公式:pq2、“只有不下雨,我才骑自行车上班”。p是q必要条件,因而,可得命题公式:qp命题表示公式(2)1、“如果我进城我就去看你,除非我很累。”设:p,我进城;q,去看你;r,我很累。则有命题公式:r(pq)2、“应届高中生,得过数学或物理竞赛的一等奖,保送上北京大学。”设:p,应届高中生;p,保送上北京大学;r,得过数学一等奖;t,得过物理一等奖。则有命题公式:p(rt)q数理逻辑的基本定义合取式:p与q,记做p∧q析取式:p或q,记做p∨q蕴含式:如果p则q,记做p→q等价式:p当且仅当q,记做p=q若A无成假赋值,则称A为重言式或永真式;若A无成真赋值,则称A为矛盾式或永假式;若A至少有一个成真赋值,则称A为可满足的;析取范式:仅由有限个简单合取式组成的析取式合取范式:仅由有限个简单析取式组成的合取式数理逻辑的基本等值式(24个)交换律:p∨qq∨p;p∧qq∧p结合律:(p∨q)∨rp∨(q∨r);(p∧q)∧rp∧(q∧r)分配律:p∨(q∧r)(p∨q)∧(p∨r);p∧(q∨r)(p∧q)∨(p∧r)双重否定律:p~~p等幂律:pp∨p;pp∧p摩根律:~(p∨q)~p∧~q;~(p∧q)~p∨~q吸收律:p∨(p∧q)p;p∧(p∨q)p同一律:p∨0p;p∧1p零律:p∨11p∧00排中律:p∨~p1矛盾律:p∧~p0蕴含等值式:p→q~p∨q等价等值式:pq(p→q)∧(q→p)假言易位式:p→q~p→~q等价否定等值式:pq~p~q归谬论:(p→q)∧(p→~q)~p合取范式合取范式:单元子句、单元子句的或(∨)的与(∧)。如:P∧(P∨Q)∧(~P∨Q)例:求取P∧(Q→R)→S的合取范式解: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)注意:首先一定要将原有的命题公式整理、转换成为各个或语句的与,不然后续推导没有意义。转换是基于数理逻辑的基本等值公式进行的,或转换到与中。思路与代数学的提取公因式方法相似。子句集命题公式的子句集S是合取范式形式下的子命题(元素)的集合。子句集是合取范式中各个合取分量的集合,生成子句集的过程可以简单地理解为将命题公式的合取范式中的与符号“∧”,置换为逗号“,”。上例转换的合取范式:(~P∨S∨Q)∧(~P∨S∨~R)其子句集为S={~P∨S∨Q,~P∨S∨~R}又如,有命题公式:P∧(P∨Q)∧(~P∨Q)其子句集S:S={P,P∨Q,~P∨Q}2.2.2命题逻辑的归结归结法推理的核心是求两个子句的归结式,因此需要先讨论归结式的定义和性质。归结式的定义设C1和C2是子句集中的任意两个子句,如果C1中的文字L1与C2中的文字L2互补,那么可从C1和C2中分别消去L1和L2,并将C1和C2中余下的部分按析取关系构成一个新子句C12,则称这一个过程为归结,称C12为C1和C2的归结式,称C1和C2为C12的亲本子句。例如:有子句:C1=P∨C1’,C2=~P∨C2’存在互补对P和~P,则可得归结式:C12=C1'∨C2'注意:C1ΛC2→C12,反之不一定成立。归结式是原两子句的逻辑推论证明归结式是原两子句的逻辑推论,或者说任一使C1、C2为真的解释I下必有归结式C12也为真。证明:设I是使C1,C2为真的任一解释,若I下的P为真,从而~P为假,必有I下C2‘为真,故C12为真。若不然,在I下P为假,从而I下C1’为真,故I下C12为真。于是C1∧C2为真。于是C1∧C2→R(C1,C2)成立。反之不一定成立,因为存在一个使C1‘∨C2’为真的解释I,不妨设C1‘为真,C2’为假。若P为真,则~P∨C2‘就为假了。因此反之不一定成立。由此可得归结式的性质。归结式的性质:归结式C12是亲本子句C12和C12的逻辑结论。命题逻辑的归结法推理过程命题逻辑的归结过程也就是推理过程。推理是根据一定的准则由称为前提条件的一些判断导出称为结论的另一些判断的思维过程。命题逻辑的归结方法推理过程:1.建立待归结命题公式首先根据反证法将所求证的问题转化成为命题公式,求证其是矛盾式(永假式)。2.求取合取范式3.建立子句集4.归结归结步骤归结法是在子句集S的基础上通过归结推理规则得到的,归结过程的最基本单元是得到归结式的过程。从子句集S出发,对S的子句间使用归结推理规则,并将所得归结式仍放入到S中(注意:此过程使得子句集不断扩大,是造成计算爆炸的根本原因),进而再对新子句集使用归结推理规则。重复使用这些规则直到得到空子句。这便说明S是不可满足的,从而与S所对应的定理是成立的。归结步骤:1)对子句集中的子句使用归结规则2)归结式作为新子句加入子句集参加归结3)归结式为空子句□为止。(证明完毕)得到空子句□,表示S是不可满足的(矛盾),故原命题成立。例题2-1:证明公式:(P→Q)→(~Q→~P)证明:(1)根据归结原理,将待证明公式转化成待归结命题公式:(P→Q)∧~(~Q→~P)(2)分别将公式前项化为合取范式:P→Q=~P∨Q结论求~后的后项化为合取范式:~(~Q→~P)=~(Q∨~P)=~Q∧P两项合并后化为合取范式:(~P∨Q)∧~Q∧P(3)则子句集为:{~P∨Q,~Q,P}(4)对子句集中的子句进行归结可得:1.~P∨Q2.~Q3.P4.Q(1,3归结)5.(2,4归结)由上可得原公式成立。2.3谓词逻辑归结法基础由于谓词逻辑与命题逻辑不同,有量词、变量和函数,所以在生成子句集之前要对逻辑公式做处理,具体的说就是要将其转化为Skolem标准形,然后在子句集的基础上再进行归结,虽然基本的归结的基本方法都相同,但是其过程较之命题公式的归结过程要复杂得多。本节针对谓词逻辑归结法介绍Skolem标准形、子句集等一些必要的概念和定理。前束范式前束范式:A是一个前束范式,如果A中的一切量词都位于该公式的最左边(不含否定词),且这些量词的辖域都延伸到公式的末端。前束范式A的形式为:(Q1x1)(Q2x2)…(Qnxn)M(x1,x2,…,xn)即:把所有的量词都提到前面去。注意:由于所有的量词的辖域都延伸到公式的末端,即,最左边量词将约束表达式中的所有同名变量。所以将量词提到公式最前端时存在约束变量换名问题。要严守规则。约束变量换名规则:(Qx)M(x)(Qy)M(y)(Qx)M(x,z)(Qy)M(y,z)量词否定等值式:~(x)M(x)(y)~M(y)~(x)M(x)(y)~M(y)量词分配等值式:(x)(P(x)∧Q(x))(x)P(x)∧(x)Q(x)(x)(P(x)∨Q(x))(x)P(x)∨(x)Q(x)消去量词等值式:设个体域为有穷集合(a1,a2,…an)(x)P(x)P(a1)∧P(a2)∧…∧P(an)(x)P(x)P(a1)∨P(a2)∨…∨P(an)量词辖域收缩与扩张等