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均取假值。但一命题的解释通常有无穷多种，
3、不可能一一测试。为此，Herbrand建议使用一种方法：从众多的解释中，选择一种代表性的解释，并严格证明：任何命题，一旦证明为在这种解释中取假值，即在所有的解释中取假值，这就是Herbrand解释。,6,3.4 命题逻辑的归结法,要证明： A1A2A3B 是定理（重言式） A1A2A3 B 是矛盾(永假)式归结推理方法就是从A1A2A3 B 出发，使用归结推理规则来寻找矛盾，最后证明定理成立。归结法（消解法）的本质是数学中的反证法，称为“反演推理方法”。,等价于,7,3.4.1 建立子句集,首先，把A1A2A3 B化成一种称作子句形的标准形式。如： P(QR)(PQ)(PQR)然后将合取范式写
4、成集合的表示形式，得 S = P, QR, PQ, PQR, 以“,”代 替“”。,子句集,一个子句,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对应的定理成立,推理结束,是,否
5、,10,例：证明(PQ)QP,先将(PQ)Q(P)化成合取范式，得 (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标准形（即与或句）,对给定的一
6、阶谓词逻辑公式G=A1A2A3B第一步，化成与其等值的前束范式 方法：参见2.3节“与或句演绎系统”第二步，化成合取范式第三步，将所有存在量词（ ）消去,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化成SK
7、OLEM标准形G的子句集子句集S中的变量，都认为是由全称量词约束着，子句间是合取关系。,15,第一类：代数、几何证明（定理证明）例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, S
8、A3, SB ,17,第二类 机器人动作问题,例2.猴子香蕉问题已知一串香蕉挂在天花板上，猴子直接去拿是够不到的，但猴子可以走动，也可以爬上梯子来达到吃香蕉的目的。,分析：问题描述，不能忽视动作的先后次序，体现时间概念。常用方法是引入状态S来区分动作的先后，以不同的状态表现不同的时间，而状态间的转换由一些算子（函数）来实现。,初始状态S0,18,解：引入谓词P(x,y,z,s): 表示猴子位于x处，香蕉位于y处，梯子位于z处，状态为sR(s): 表示s状态下猴子吃到香蕉ANS(s): 表示形式谓词，只是为求得回答的动作序列而虚设的。引入状态转移函数Walk(y, z, s): 表示原状态s下，
9、在walk作用下，猴子从y走到z处所建立的新状态。Carry(y,z,s): 表示原状态s下，在Carry作用下，猴子从y搬梯子到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,寄存
10、器a,b,c分别放入u,x,y,z时的状态为sLoad(x,s):表示状态s下,对任一寄存器x来说,实现(x)A后的新状态Add(x,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是不可满足的当且仅
11、当S是不可满足的。（证明从略，石纯一AI原理P1720). 由于个体变量论域D的任意性，以及解释的个数的无限性，对一个谓词公式来说，不可满足性的证明是困难的。 如果对一个具体的谓词公式能找到一个较简单的特殊的论域，使得只要在该论域上该公式是不可满足的，便能保证在任何论域上也是不可满足的，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
12、(t1,tn)是出现于G中的任一函数符号，而t1, t2, ,tn是Hi-1的元素，I=1,2,H为G的H域。（或说是相应子句集S的H域） “可数集合”H是直接依赖于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
13、为真的问题。子句集S在D上不满足问题成了H上不满足问题，这是很有意义的结果。,29,定理3.3.2(1)设I是S的论域D上的解释，存在对应于I的H解释I*，使得S|I=T，必有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分枝上所标
14、记的所有文字的并集。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,完全语义树：对所有结点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
15、),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(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的完全语义树都是一棵
16、有限的封闭语义树。（注：证明从略）定理3.3.4(2)S是不可满足的，当且仅当存在不可满足的S的有限基例集。（注：证明从略）,36,应当指出：,Herbrand定理给出了一阶逻辑的半可判定算法，即仅当被证定理是成立的，使用该算法可得证，否则，得不出任何结果。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出
17、现于S中，而L不出现于S中，便说L为S的纯文字。 S中删除LS=，S可满足 S中删除LS，S,S同时不可满足分离规则S=LA1) (LAm)(LB1) (LBn)R（不含L和L的子句等） S=A1,Am,R S=B1,Bn,R S不可满足 S、 S同时不可满足,38,3.7 归结原理,虽然Herbrandp定理给出了推理算法，但需逐次生成基例集 ，再检验 的不可满足性，常常难以实现。 1965年，Robinson提出了归结原理，是对自动推理的重大突破。,39,3.7.1 置换与合一,置换：是形为t1/v1,tn/vn的一个有限集。其中，vi是变量，而ti是不同于vi的项（常量、变量、函数）且v
18、ivj，（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中出现的变量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 =u
19、1/y1,um/ym置换乘积是新的置换，作用于E相当于先后对E的作用。定义如下：先作置换：t1 /x1 , tn /xn , u1 /y1,um/ym 若yix1, xn时，先从中删除ui/yi；ti = xi时，再从中删除ti / xi；所设的置换称作与的乘积，记作,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),
20、 (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的最一般置换，记作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
21、)/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=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
22、(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(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(
23、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.注：不可合一的情况 不存在vk变量，如w=P(a,b,c),P(d,b,c) 不存在tk变量，如w=P(a,b),P(x,y,z)出现不一致集为x,f(x
24、)形,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,例1 C1 = A(x) B(x) C2 = A(g(x)【解】：先将C1的变量x改写为y，可得mgu = g(x
25、)/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的二元归结式。最简单的例子是：C1 = P Q， C
26、2 = 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的因子的二元归结
27、式（4） C1的因子和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月修改,
