归结推理方法ppt课件.ppt

《归结推理方法ppt课件.ppt》由会员分享，可在线阅读，更多相关《归结推理方法ppt课件.ppt（55页珍藏版）》请在三一办公上搜索。

1、1,第三章 归结原理（第二部分）(Chapter 3 Resolution Reasoning)(Part B),徐从富浙江大学人工智能研究所2002年第一稿2004年9月修改,2,本章的主要参考文献：1 石纯一 等.人工智能原理.清华大学出版社,1993.pp11-81.（【注意】：本课件以该书中的这部分内容为主而制作，若想更加全面地了解归结原理及其应用，请参见如下文献2和3）2 陆汝钤.人工智能（下册）.科学出版社,2000.pp681-728.3 王永庆.人工智能原理与方法.西安交通大学出版社,1998.pp111-155.【注】：若对定理的机械化证明的更多内容感兴趣者，可参考陆汝钤.人

2、工智能（下册）.科学出版社,2000.pp729-788.其最新进展可参考我国数学家吴文俊院士的相关论文，不过，他的研究工作对数学要求很高！,3,前言命题逻辑的归结法子句型Herbrand定理归结原理,4,归结（resolution)(也称消解）推理方法：,这是一种机械化的可在计算机上加以实现的推理方法。AI程序设计语言Prolog就是基于归结原理的一种逻辑程序设计语言。,5,归结法（也称消解法）的本质是一种反 证法。为了证明一个命题A恒真，要证明其反命题A恒假。所谓恒假就是不存在模型，即在所有的可能解释中，A均取假值。但一命题的解释通常有无穷多种，不可能一一测试。为此，Herbrand建议使

3、用一种方法：从众多的解释中，选择一种代表性的解释，并严格证明：任何命题，一旦证明为在这种解释中取假值，即在所有的解释中取假值，这就是Herbrand解释。,6,3.4 命题逻辑的归结法,要证明：A1A2A3B 是定理（重言式）A1A2A3 B 是矛盾(永假)式归结推理方法就是从A1A2A3 B 出发，使用归结推理规则来寻找矛盾，最后证明定理成立。归结法（消解法）的本质是数学中的反证法，称为“反演推理方法”。,等价于,7,3.4.1 建立子句集,首先，把A1A2A3 B化成一种称作子句形的标准形式。如：P(QR)(PQ)(PQR)然后将合取范式写成集合的表示形式，得 S=P,QR,PQ,PQR,

4、以“,”代 替“”。,子句集,一个子句,8,3.4.2 归结式,设C1=PC1 C2=PC2 消去互补对，新子句 R(C1,C2)=C1 C2没有互补对的两子句没有归结式，归结推理即对两子句做归结证明 C1C2R(C1,C2)任一使C1，C2为真的解释I下必有R(C1,C2)也是真。空子句当C1=P C2=P两个子句的归结式为空，记作，称为空子句，体现了矛盾。,为两个子句,子句C1、C2的归结式,9,3.4.3归结推理过程,子句集S,归结推理规则,S空子句,S=所得归结式,说明S是不可满足的,与S对应的定理成立,推理结束,是,否,10,例：证明(PQ)QP,先将(PQ)Q(P)化成合取范式，得

5、(PQ)QP建立子句集 S=PQ,Q,P)对S作归结PQQPP 1),2)归结 3),4)归结 证毕注：一阶谓词逻辑的归结方法比命题逻辑的归结法要复杂得多，原因是要对量词和变量做专门的处理。,11,3.5 子句形,设有由一阶谓词逻辑描述的公式A1，A2，A3和B，证明在A1A2A3成立的条件下有B成立。仍然采用反演法来证明。A1A2A3B(3.2.1)是不可满足的。与命题逻辑不同，首先遇到了量词问题，为此要将(3.2.1)式化成SKOLEM标准形。,12,3.5.1 SKOLEM标准形（即与或句）,对给定的一阶谓词逻辑公式G=A1A2A3B第一步，化成与其等值的前束范式 方法：参见2.3节“与

6、或句演绎系统”第二步，化成合取范式第三步，将所有存在量词（）消去,13,3.5.2子句与子句集,概念原子公式：不含有任何联结词的谓词公式文字：原子或原子的否定子句：一些文字的析取如，P(x)Q(x,y),P(x,c)R(x,y,f(x)都是子句由于G的SKOLEM标准形的母式已为合取范式，从而母式的每一个合取项都是一个子句，可以说，母式是由一些子句的合取组成的。子句集S：将G的已消去存在量词的SKOLEM标准形，再略去全称量词，最后以“,”代替合取符号“”，便得子句集S。,14,例：,解：将G化成SKOLEM标准形G的子句集子句集S中的变量，都认为是由全称量词约束着，子句间是合取关系。,15,

7、第一类：代数、几何证明（定理证明）例1.证明梯形的对角线与上下底构成的内错角相等,3.5.3 建立子句集举例,16,证明：设梯形的顶点依次为a,b,c,d.引入谓词：T(x,y,u,v)表示以xy为上底，uv为下底的梯形P(x,y,u,v)表示xy/uvE(x,y,z,u,v,w)表示xyz=uvw问题的逻辑描述和相应的子句集为梯形上下底平行：平形内错角相等已知条件要证明的结论：B:E(a,b,d,c,d,b)结论的“非”：SB:E(a,b,d,c,d,b)从而 S=SA1,SA2,SA3,SB,17,第二类 机器人动作问题,例2.猴子香蕉问题已知一串香蕉挂在天花板上，猴子直接去拿是够不到的，

8、但猴子可以走动，也可以爬上梯子来达到吃香蕉的目的。,分析：问题描述，不能忽视动作的先后次序，体现时间概念。常用方法是引入状态S来区分动作的先后，以不同的状态表现不同的时间，而状态间的转换由一些算子（函数）来实现。,初始状态S0,18,解：引入谓词P(x,y,z,s):表示猴子位于x处，香蕉位于y处，梯子位于z处，状态为sR(s):表示s状态下猴子吃到香蕉ANS(s):表示形式谓词，只是为求得回答的动作序列而虚设的。引入状态转移函数Walk(y,z,s):表示原状态s下，在walk作用下，猴子从y走到z处所建立的新状态。Carry(y,z,s):表示原状态s下，在Carry作用下，猴子从y搬梯子

9、到z处所建立的新状态。Climb(s):表示原状态s下，在Climb作用下，猴子爬上梯子所建立的新状态。,19,初始状态为S0，猴子位于a，香蕉位于b,梯子位于c，问题描述如下：猴子走到梯子处（从x z）猴子搬着梯子到y处猴子爬上梯子吃到香蕉初始条件结论,walk,20,第三类 程序设计自动化问题,例3：简单的程序集合问题若一台计算机有寄存器a,b,c和累加器A，要求自动设计实现+(b)c的程序。,21,解:先引入谓词P(u,x,y,z,s):表示累加器A,寄存器a,b,c分别放入u,x,y,z时的状态为sLoad(x,s):表示状态s下,对任一寄存器x来说,实现(x)A后的新状态Add(x,

10、s):表示状态s下,对任一寄存器x来说,实现(x)+(A)A后的新状态Store(x,s):表示状态s下,对任一寄存器x来说,实现(A)x后的新状态问题描述(a)A):寄存器a中的值放入寄存器A中(b)+(A)A),22,(A)C)初始状态D下，累加器A与寄存器a,b,c中的数值结论子句集 S=SA1,SA2,SA3,SA4,SB,23,3.6 Herbrand定理,虽然公式G与其子句集S并不等值，但它们在不可满足的意义下又是一致的。亦即，G是不可满足的当且仅当S是不可满足的。（证明从略，石纯一AI原理P1720).由于个体变量论域D的任意性，以及解释的个数的无限性，对一个谓词公式来说，不可满

11、足性的证明是困难的。如果对一个具体的谓词公式能找到一个较简单的特殊的论域，使得只要在该论域上该公式是不可满足的，便能保证在任何论域上也是不可满足的，Herbrand域（简称H域）具有这样的性质。,24,3.6.1 H域,设G是已给的公式，定义在论域D上，令H0是G中所出现的常量的集合，若G中没有常量出现，就任取常量aD，而规定H0=a即 H0=若G中有常量，为G中常量的集合 若无常量，则为aHi=Hi-1 U 所有形如f(t1,tn)的元素其中，f(t1,tn)是出现于G中的任一函数符号，而t1,t2,tn是Hi-1的元素，I=1,2,H为G的H域。（或说是相应子句集S的H域）“可数集合”H是

12、直接依赖于G的最多共有可数个元素的集合,25,例1.S=P(a),P(x)P(f(x),26,例2.S=P(x),Q(f(x,a)R(b)【注】：在S中出现函数f(x,a),仍视为f(x1,x2)的形式,27,概念基原子 原子基文字 文字基子句 子句基子句集 子句集基例：对：基子句：基例：,:没有变量出现的,28,3.6.2 H解释,思想：由子句集S建立H域、原子集A，使任一论域D上S为真的问题，化成了仅有可数个元素的H域上S为真的问题。子句集S在D上不满足问题成了H上不满足问题，这是很有意义的结果。,29,定理3.3.2(1)设I是S的论域D上的解释，存在对应于I的H解释I*，使得S|I=T

13、，必有S|I*=T。定理3.3.2(2)子句集S是不可满足的，当且仅当在所有的S的H解释下为假。（注：该定理将S在一般论域上的不可满足问题化成了可数集上H上的不可满足问题，以上只需讨论在S的H上即可。）定理3.3.2(3)子句集S是不可满足的当且仅当对每个解释I下，至少有S的某个子句的某个基例为假。,30,例1：设子句集S的原子集A=P,Q,R,图 语义树（二叉树）,3.6.3 语义树,I(N)表示：从根结点到结点N分枝上所标记的所有文字的并集。I(N34)=P,Q,R,31,例2：解：H=a,f(a),f(f(a),A=P(a),Q(a),P(f(a),Q(f(a),N38,32,完全语义树

14、：对所有结点N,（）,I(N)包含了A=A1,A2,中的 或Ai，i=1,2,n。失败结点：如果结点N的I(N)使S的某一子句有某一基例为假，而N的父辈结点不能判断这个事实，就说N是失败结点。封闭树：如果S的完全语义树的每个分枝上都有一个失败结点，即为封闭树。,33,例2中的完全语义树即为封闭树。,图 封闭语义树,N0,N11,N12,N21,N22,N24,N31,N32,N4,13,N4,14,N36,P(a),P(a),Q(a),Q(a),P(f(a),如，I(N2,2)=P(a),Q(a),使得S中，P(a)Q(a)为假。I(N3,6)=P(a),Q(a),P(f(a),使得S中的P(

15、f(a)为假。I(N4,1)=P(a),Q(a),使得Q(f(y)为假。,N38,N41,N42,N49,N4,10,34,3.6.4 Herbrand定理,一阶谓词描述A1A2 A3B化成不满足问题G=A1A2 A3 BG化成SKOLEM形S=,一般论域D简化成H域上的讨论引入语义树,35,Herbrand给出的两个定理,定理3.3.4(1)子句集S是不可满足的，当且仅当对应于S的完全语义树都是一棵有限的封闭语义树。（注：证明从略）定理3.3.4(2)S是不可满足的，当且仅当存在不可满足的S的有限基例集。（注：证明从略）,36,应当指出：,Herbrand定理给出了一阶逻辑的半可判定算法，即

16、仅当被证定理是成立的，使用该算法可得证，否则，得不出任何结果。Herbrand定理已将证明问题化成了命题逻辑问题，所以只需在命题逻辑范围内简化。,37,补充：石纯一编著：人工智能原理P3940重言式子句可删除规则 S=PP,C1,C2S=C1,C2.单文字删除规则 S=L，LC1，L C2，C3，C4S=L C2，C3，C4，删除含L的子句 S=C2，C3，C4，删除文字L纯文字删除规则 当文字L出现于S中，而L不出现于S中，便说L为S的纯文字。S中删除LS=，S可满足 S中删除LS，S,S同时不可满足分离规则S=LA1)(LAm)(LB1)(LBn)R（不含L和L的子句等）S=A1,Am,R

17、 S=B1,Bn,R S不可满足 S、S同时不可满足,38,3.7 归结原理,虽然Herbrandp定理给出了推理算法，但需逐次生成基例集，再检验 的不可满足性，常常难以实现。1965年，Robinson提出了归结原理，是对自动推理的重大突破。,39,3.7.1 置换与合一,置换：是形为t1/v1,tn/vn的一个有限集。其中，vi是变量，而ti是不同于vi的项（常量、变量、函数）且vivj，（ij),i,j=1,2,n例如，a/x,b/y,f(x)/z,f(z)/x,y/z都是置换。空置换：不含任何元素的置换。令置换=t1/v1,t2/v2,tn/vn E是一阶谓词 作用于E，就是将E中出现

18、的变量vi均以ti代入（i=1,2,n)，以E表示结果，并称为E的一个例。作用于项t，是将t中出现的变量vi以ti代入(i=1,n)，结果以t表示。,40,例：=a/x,f(b)/y,u/z E=P(x,y,z)t=g(x,y)那么 E=P(a,f(b),u)t=g(a,f(b),41,常使用的置换的运算是置换乘法（合成）若=t1/x1,tn/xn=u1/y1,um/ym置换乘积是新的置换，作用于E相当于先后对E的作用。定义如下：先作置换：t1/x1,tn/xn,u1/y1,um/ym 若yix1,xn时，先从中删除ui/yi；ti=xi时，再从中删除ti/xi；所设的置换称作与的乘积，记作,

19、42,例：=f(y)/x,z/y=a/x,b/y,y/z 求解：先做置换 f(y)/x,z/y,a/x,b/y,y/z 即 f(b)/x,y/y,a/x,b/y,y/z 先删除a/x,b/y,再删y/y，得=f(b)/x,y/z 当 E=P(x,y,z)时，E=P(f(y),z,z),(E)=P(f(b),y,y)E()=P(f(b),y,y),(E)=E(),43,概念：合一,设有公式集E1,Ek和置换，使E1=E2=Ek 称E1,Ek是可合一的，且称为合一置换（union replacement）。若E1,Ek有合一置换，且对E1,Ek的任一合一置换都有置换存在，使得=便说是E1,Ek的最

20、一般置换，记作mgu（most general replacement),44,例1 E1=P(a,y),E2=P(x,f(b),E1,E2可合一，=a/x,f(b)/y,且是E1，E2的mgu.例2 E1=P(x),E2=P(f(y)置换=f(a)/x,a/y并不是E1、E2的mgu，而=f(y)/x才是E1、E2的mgu，也可以说，是E1、E2的最简单合一置换。,45,例3 E1=P(x),E2=P(y)。显然y/x和x/y都是E1、E2的mgu，说明mgu不唯一。,46,求mgu的算法（最一般合一置换mgu),令w=E1,E2。令k=0,w0=w,0=(空置换）。如果wk已合一，停止，k

21、=mgu。否则找不一致集。若Dk中存在元素vk,tk,其中vk不出现于tk中做 5，否则不可合一。令k+1=ktk/vkwk+1=wktk/vk=wk+1。k+1k 转 3。,47,例 w=P(a,x,f(g(y),P(z,f(a),f(u)其中，E1=P(a,x,f(g(y),E2=P(z,f(a),f(u)求 E1,E2的mug解：(1)w=P(a,x,f(g(y),P(z,f(a),f(u).(2)0=,w0=w.(3)w0未合一，自左至右找不一致集，有D0=a,z.(4)取v0=z,t0=a.(5)令1=0，t0/v0=a/z=a/z.w1=w01=P(a,x,f(g(y),P(a,f

22、(a),f(u).(3)w1未合一，不一致集D1=x,f(a).(4)取v1=x,t1=f(a).(5)令2=1f(a)/x=a/z,f(a)/x=a.z,f(a)/x w2=w12=P(a),f(a),f(g(y),p(a,f(a),f(u).,48,(3)w2未合一，不一致集D2=g(y),u.(4)取v2=u,t2=g(y).(5)令3=2g(y)/u=a/z,f(a)/xg(y)/u=a/z,f(a)/x,g(y)/u.w3=w23=P(a),f(a),f(g(y),P(a),f(a),f(g(y)(3)w3已合一，这时3=a/z,f(a)/x,g(y)/u，即为E1，E2的mgu.注

23、：不可合一的情况 不存在vk变量，如w=P(a,b,c),P(d,b,c)不存在tk变量，如w=P(a,b),P(x,y,z)出现不一致集为x,f(x)形,49,3.7.2 归结式,在谓词逻辑下求两个子句的归结式，和命题逻辑一样是消去互补对，但需考虑变量的合一和置换。二元归结式：设C1,C2是两个无公共 变量的子句，L1,L2分别是C1,C2的文字，若L1与 L2有mgu，则(C1-L1)(C2-L2)称作子句C1,C2的一个二元归结式，而L1,L2为被归结的文字。【注意】：同命题逻辑下的归结式不同的是，先需对C1,C2有关变量作mgu，再消去互补对。同样有：C1 C2 R(C1,C2),50

24、,例1 C1=A(x)B(x)C2=A(g(x)【解】：先将C1的变量x改写为y，可得mgu=g(x)/y，作归结得R(C1,C2)=B(g(x)。例2 C1=P(x)Q(x)C2=P(g(y)Q(b)R(x)【解】：可知有两个合一置换，故有两个二元归结式。（1）当取=g(y)/x时，得R(C1,C2)=Q(g(y)Q(b)R(x)（2）当取=b/x时，得R(C1,C2)=P(b)P(g(y)R(x),51,例3 C1=P(x)Q(b)C2=P(a)Q(y)R(z)【解】：这时要注意，求归结式不能同时消去两个互补对。如在=a/x,b/y下，得R(z)。这不是C1,C2的二元归结式。最简单的例子

25、是：C1=P Q，C2=P Q若消去上述两个互补对便得空子句。但是C1,C2并无矛盾。这说明消去两个互补对的结果并不是C1,C2的逻辑推论了。因此，消去两个互补对结果不是二元归结式。,52,在对子句作归结前，可先考虑子句内部的化简，这便提出了子句因子的概念。设 C=P(x)P(f(y)Q(x)令=f(y)/x，将置换使用于C，可使P(x),P(f(y)合一。显然C比C简单得多。子句因子：若一个子句C的几个文字有mgu，那么C的C称作子句C的因子。定义：若C1,C2是无公共变量的子句，作（1）C1,C2的二元归结式（2）C1的因子和C2的二元归结式（3）C1,和C2的因子的二元归结式（4）C1的

26、因子和C2的因子的二元归结式这四种二元归结式都叫子句C1,C2的归结式，记作R(C1,C2),53,例4 C1=P(x)P(f(y)Q(g(y)C2=P(f(g(a)Q(b)【解】：先作C1的因子，取=f(y)/x，得C1的因子C1=P(f(y)Q(g(y)于是C1,C2归结式为R(C1,C2)=Q(g(g(a)Q(b)【说明】：上述推理过程的正确性能得到保证。,54,3.7.3 归结推理过程,为证明AB成立，其中A,B是谓词公式，使用反演过程，先建立G=A B 进而做出相应的子句集S，只需证明S是不可满足的。归结法是仅有一条推理规则的推理方法。对S中的可归结的子句作归结，求得归结式，并将这归结式（新子句）仍放入S中，反复进行这个归结过程直至产生空子句为止。这时S必是不可满足的，从而证明AB是成立的。【注意】：归结推理的实例请详见石纯一等编著的人工智能原理pp48-51。,55,Thanks！2002年第一稿2004年9月修改,