归结推理方法

1第三章归结原理（第二部分）(Chapter3ResolutionReasoning)(PartB)徐从富浙江大学人工智能研究所2002年第一稿2004年9月修改2本章的主要参考文献：[1]石纯一等.《人工智能原理》.清华大学出版社,1993.pp11-81.（【注意】：本课件以该书中的这部分内容为主而制作，若想更加全面地了解归结原理及其应用，请参见如下文献[2]和[3]）[2]陆汝钤.《人工智能》（下册）.科学出版社,2000.pp681-728.[3]王永庆.《人工智能原理与方法》.西安交通大学出版社,1998.pp111-155.【注】：若对定理的机械化证明的更多内容感兴趣者，可参考陆汝钤.《人工智能》（下册）.科学出版社,2000.pp729-788.其最新进展可参考我国数学家吴文俊院士的相关论文，不过，他的研究工作对数学要求很高！3•前言•命题逻辑的归结法•子句型•Herbrand定理•归结原理4归结（resolution)(也称消解）推理方法：这是一种机械化的可在计算机上加以实现的推理方法。AI程序设计语言Prolog就是基于归结原理的一种逻辑程序设计语言。5归结法（也称消解法）的本质是一种反证法。为了证明一个命题A恒真，要证明其反命题~A恒假。所谓恒假就是不存在模型，即在所有的可能解释中，~A均取假值。但一命题的解释通常有无穷多种，不可能一一测试。为此，Herbrand建议使用一种方法：从众多的解释中，选择一种代表性的解释，并严格证明：任何命题，一旦证明为在这种解释中取假值，即在所有的解释中取假值，这就是Herbrand解释。63.4命题逻辑的归结法要证明：A1∧A2∧A3B是定理（重言式）A1∧A2∧A3∧~B是矛盾(永假)式归结推理方法就是从A1∧A2∧A3∧~B出发，使用归结推理规则来寻找矛盾，最后证明定理成立。归结法（消解法）的本质是数学中的反证法，称为“反演推理方法”。等价于73.4.1建立子句集首先，把A1∧A2∧A3∧~B化成一种称作子句形的标准形式。如：P∧(Q∨R)∧(~P∨~Q)∧(P∨~Q∨R)然后将合取范式写成集合的表示形式，得S={P,Q∨R,~P∨~Q,P∨~Q∨R},以“,”代替“∧”。子句集一个子句83.4.2归结式1.设C1=P∨C1′C2=~P∨C2′消去互补对，新子句R(C1,C2)=C1′∨C2′没有互补对的两子句没有归结式，归结推理即对两子句做归结2.证明C1∧C2R(C1,C2)任一使C1，C2为真的解释I下必有R(C1,C2)也是真。3.空子句□当C1=PC2=~P两个子句的归结式为空，记作□，称为空子句，体现了矛盾。为两个子句子句C1、C2的归结式93.4.3归结推理过程子句集S归结推理规则S′＝空子句□S′=所得归结式说明S是不可满足的与S对应的定理成立推理结束是否10例：证明(PQ)∧~Q~P先将(PQ)∧~Q∧~(~P)化成合取范式，得(~P∨Q)∧~Q∧P建立子句集S={~P∨Q,~Q,P)对S作归结1)~P∨Q2)~Q3)P4)~P1),2)归结5)□3),4)归结证毕注：一阶谓词逻辑的归结方法比命题逻辑的归结法要复杂得多，原因是要对量词和变量做专门的处理。113.5子句形设有由一阶谓词逻辑描述的公式A1，A2，A3和B，证明在A1∧A2∧A3成立的条件下有B成立。仍然采用反演法来证明。A1∧A2∧A3∧~B(3.2.1)是不可满足的。与命题逻辑不同，首先遇到了量词问题，为此要将(3.2.1)式化成SKOLEM标准形。123.5.1SKOLEM标准形（即与或句）对给定的一阶谓词逻辑公式G=A1∧A2∧A3∧~B第一步，化成与其等值的前束范式[方法：参见2.3节“与或句演绎系统”]第二步，化成合取范式第三步，将所有存在量词（）消去133.5.2子句与子句集1.概念1)原子公式：不含有任何联结词的谓词公式2)文字：原子或原子的否定3)子句：一些文字的析取如，P(x)∨~Q(x,y),~P(x,c)∨R(x,y,f(x))都是子句由于G的SKOLEM标准形的母式已为合取范式，从而母式的每一个合取项都是一个子句，可以说，母式是由一些子句的合取组成的。4)子句集S：将G的已消去存在量词的SKOLEM标准形，再略去全称量词，最后以“,”代替合取符号“∧”，便得子句集S。14例：S.z))y,R(x,z)(Q(x,z))y,R(x,y)P(x,z)((~y)(x)((G求其子句集解：①将G化成SKOLEM标准形G的子句集子句集S中的变量，都认为是由全称量词约束着，子句间是合取关系。g(x))))f(x),R(x,g(x))(Q(x,g(x)))f(x),R(x,f(x))P(x,x)((~(Gg(x))}f(x),R(x,g(x))(Q(x,g(x)),f(x),R(x,f(x))P(x,{~S15第一类：代数、几何证明（定理证明）例1.证明梯形的对角线与上下底构成的内错角相等3.5.3建立子句集举例a(x)d(v)b(y)c(u)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②问题的逻辑描述和相应的子句集为i.梯形上下底平行：ii.平形内错角相等iii.已知条件iv.要证明的结论：B:E(a,b,d,c,d,b)结论的“非”：S~B:~E(a,b,d,c,d,b)}从而S={SA1,SA2,SA3,S~B}v)u,y,P(x,v)u,y,T(x,:~SAv))u,y,P(x,v)u,y,v)(T(x,u)(y)(x)((:A11y)v,u,v,y,E(x,v)u,y,P(x,:~Sy))v,u,v,y,E(x,v)u,y,v)(P(x,u)(y)(x)((:AA21d)c,b,T(a,:Sd)c,b,T(a,:AA3317第二类机器人动作问题例2.猴子香蕉问题已知一串香蕉挂在天花板上，猴子直接去拿是够不到的，但猴子可以走动，也可以爬上梯子来达到吃香蕉的目的。分析：问题描述，不能忽视动作的先后次序，体现时间概念。常用方法是引入状态S来区分动作的先后，以不同的状态表现不同的时间，而状态间的转换由一些算子（函数）来实现。(b)y(a)x(c)z初始状态S018解：1)引入谓词P(x,y,z,s):表示猴子位于x处，香蕉位于y处，梯子位于z处，状态为sR(s):表示s状态下猴子吃到香蕉ANS(s):表示形式谓词，只是为求得回答的动作序列而虚设的。2)引入状态转移函数Walk(y,z,s):表示原状态s下，在walk作用下，猴子从y走到z处所建立的新状态。Carry(y,z,s):表示原状态s下，在Carry作用下，猴子从y搬梯子到z处所建立的新状态。Climb(s):表示原状态s下，在Climb作用下，猴子爬上梯子所建立的新状态。193)初始状态为S0，猴子位于a，香蕉位于b,梯子位于c，问题描述如下：a)猴子走到梯子处（从xz）b)猴子搬着梯子到y处c)猴子爬上梯子吃到香蕉d)初始条件e)结论s))z,walk(x,z,y,P(z,s)z,y,P(x,:~Ss)))z,walk(x,z,y,P(z,s)z,y,s)(P(x,z)(y)(x)((:AA11walks))y,carry(x,y,y,P(y,s)x,y,P(x,:~Ss)))y,carry(x,y,y,P(y,s)x,y,s)(P(x,y)(x)((:AA22)R(Climb(s)s)b,b,P(b,:~S))R(Climb(s)s)b,b,s)(P(b,(:AA33)sc,b,P(a,:S)sc,b,(P(a,:A0A404ANS(s)R(s):~Ss)R(s)(:BB~20第三类程序设计自动化问题例3：简单的程序集合问题若一台计算机有寄存器a,b,c和累加器A，要求自动设计实现(a)+(b)c的程序。21解:1)先引入谓词P(u,x,y,z,s):表示累加器A,寄存器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后的新状态2)问题描述a.((a)A):寄存器a中的值放入寄存器A中b.((b)+(A)A)s))load(a,z,y,x,P(x,s)z,y,x,P(u,:~Ss)))load(a,z,y,x,P(x,s)z,y,x,s)(P(u,z)(y)(x)(u)((:A1A1s))add(b,z,y,x,y,P(us)z,y,x,P(u,:~Ss)))add(b,z,y,x,y,P(us)z,y,x,s)(P(u,z)(y)(x)(u)((:A2A222c.((A)C)d.初始状态D下，累加器A与寄存器a,b,c中的数值e.结论子句集S={SA1,SA2,SA3,SA4,S~B}s))store(c,u,y,x,P(u,s)z,y,x,P(u,:~Ss)))store(c,u,y,x,P(u,s)z,y,x,s)(P(u,z)(y)(x)(u)((:A3A35)P(1,2,3,4,:Sd)P(1,2,3,4,:A4A4ANS(s)s)y,xy,x,P(u,:~Ss)y,xy,x,s)(P(u,y)(x)(u)((:BB~ANS(s)s)y,xy,x,P(u,:~Ss))y,xy,x,(P(u,s)(~y)(x)(u)((s)y,xy,x,s)(P(u,y)(x)(u)((~B~B~233.6Herbrand定理虽然公式G与其子句集S并不等值，但它们在不可满足的意义下又是一致的。亦即，G是不可满足的当且仅当S是不可满足的。（证明从略，石纯一《AI原理》P17~20).由于个体变量论域D的任意性，以及解释的个数的无限性，对一个谓词公式来说，不可满足性的证明是困难的。如果对一个具体的谓词公式能找到一个较简单的特殊的论域，使得只要在该论域上该公式是不可满足的，便能保证在任何论域上也是不可满足的，Herbrand域（简称H域）具有这样的性质。243.6.1H域设G是已给的公式，定义在论域D上，令H0是G中所出现的常量的集合，若G中没有常量出现，就任取常量aD，而规定H0={a}即H0=若G中有常量，为G中常量的集合若无常量，则为{a}Hi=Hi-1U{所有形如f(t1,…,tn)的元素}其中，f(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))}}f(f(a)),f(a),{a,Hf(f(a))}f(a),{a,f(f(a))}{f(a),f(a)}{a,f(a)}}{a,x|{f(x)H}Hx|{f(x)HHf(a)}{a,{f(a)}{a}{f(a)}H}Hx|{f(x)HH{a}H11120001026例2.S={P(x),Q(f(x,a))∨R(b)}【注】：在S中出现函数f(x,a),仍视为f(x1,x2)的形式b)}f(b,a),f(b,b),f(a,a),f(a,b,{a,b)}f(b,a),f(b,b),f(a,a),{f(a,b}{a,b}}{a,x2x1,|x2){f(x1,HHb}{a,H01027概念1.基原子原子2.基文字文字3.基子句子句4.基子句集子句集基例：对：①基子句：②基例：:没有变量出现的的一个基类称作所得的