第三章2消解原理.ppt

1、1,3.4 消 解 原 理,Resolution principle,2,内容提要,置换、合一 子句集的求取 9个步骤 消解推理规则 含有变量的消解式 消解反演求解,3,谓词逻辑法（predicate logic）,谓词演算 1.语法与语义 2.连词和量词 谓词公式 1.定义 2.合适公式的性质 置换与合一 1.置换 2.合一算法,4,命题,def :具有真假意义的语句 命题的真值,真,假,1+1=10,Bobs car is red,Marys uncle,5,命题逻辑有较大的局限性,无法描述客观事物的结构和逻辑特征 不能把不同事物间的共同特征表述出来,两个命题,无法把两个人都是学生这一共同

2、特征表示出来,引出谓词逻辑,6,谓词,STUDENT ( tom ) GREATER( 5,3 ),谓词名,个体,用于刻划个体的性质,状态或个体间的关系,表示某个独立存在的事物或某个抽象的概念,刻划了tom的身份特征,刻划了两个个体5和3之间的”大于”关系,7,谓词公式的定义,原子谓词公式：用P(x1,x2,xn)表示一个n元谓词公式其中P为n元谓词，x1,x2,xn为客体变量或变元。通常把P(x1,x2,xn)叫做谓词演算的原子公式，或原子谓词公式。 分子谓词公式：可以用连词把原子谓词公式组成复合谓词公式，并把它叫做分子谓词公式。,8,连词和量词,原子公式由若干谓词和个体组成,是谓词演算的基

3、本块,用连词和量词将多个原子公式组合在一起,来表示复杂的含义. 用连词来连接若干个谓词组成一个谓词公式,用量词来刻划谓词和个体的关系,合取 ,析取 ,蕴含 ,非 ,全称量词,存在量词,连词,量词,9,合取（conjunction）就是用连词把几个公式连接起来而构成的公式。合取项是合取式的每个组成部分。,例：LIKE(I，MUSIC)LIKE(I，PAINTING) (我喜爱音乐和绘画。),析取（disjunction）就是用连词把几个公式连接起来而构成的公式。析取项是析取式的每个组成部分。,例： PLAYS(LILI，BASKETBALL)PLAYS(LILI，FOOTBALL) (李力打篮球

4、或踢足球。),10,蕴涵 表示如果-那么的语句。用连词连接两个公式所构成的公式叫做蕴涵。,例: RUNS(LIUHUA,FASTEST) WINS(LIUHUA,CHAMPION) (如果刘华跑得最快，那么他取得冠军),非（NOT） 表示否定，、均可表示。,例：INROOM(ROBOT，r2) (机器人不在2号房间内。),IF P THEN Q,前项,左项,后项,右式,11,全称量词(Universal Quantifier)若一个原子公式P(x)，对于所有可能变量x都具有T值，则用( x)P(x)表示。,例：( x)ROBOT(x) COLOR(x,GRAY) (所有的机器人都是灰色的） (

5、 x)Student(x) Uniform(x,Color) (所有学生都穿彩色制服),存在量词(Existential Quantifier) 若一个原子公式P(x)，至少有一个变元X，可使P(X)为T值，则用( x)P(x)表示。,例：( x)INROOM(x,r1) (1号房间内有个物体),量化变元(Quantified Variables)被量化了的变元x-约束变量。,12,置换与合一,置换 形如t1/x1,t2/x2,tn/xn的有限集合。 其中，ti是项，xi是互不相同的变元；ti/xi表示用ti置换xi； 不允许ti与xi相同，也不允许变元xi循环地出现在另一个tj中。 合一 设

6、有公式集F=F1,F2,Fn,若存在一个置换s使得F1s=F2s=Fns，则称s是公式集F的一个合一，且称F1,F2,Fn是可合一的。,置换是不可交换的,最一般合一,13,置换举例,设有表达式Px,f(y),B ，对于置换： s1=z/x,w/y s2=A/y 分别有： Px,f(y),Bs1= Pz,f(w),B Px,f(y),Bs2= Px,f(A),B,14,合一者、最一般合一者举例,设有表达式集Ei=Px,f(y),B，Px,f(B),B， 该表达式集的合一者：s1=B/y，s2=w/x,B/y s1=B/y是该表达式集的最一般合一者。 （为什么？）,15,基本概念：对谓词演算公式进

7、行分解和化简，消去一些符号，以求得导出子句。,消解原理(resolution principle),也叫做归结原理。消解是一种可用于一定的子句公式的重要推理规则。 一子句定义为由文字的析取组成的公式(一个原子公式和原子公式的否定都叫做文字)。 当消解可使用时，消解过程被应用于母体子句对，以便产生一个导出子句。 eg，如果存在某个公理E1E2和另一公理E2E3，那么E1E3在逻辑上成立。这就是消解，而称E1E3为E1E2和E2E3的消解式(resolvent)。,任一谓词演算公式可以化成一个子句集。 其变换过程由下列九个步骤组成,16,子句集的求取,消去蕴涵符号 减少否定符号的辖域 对变量标准化

8、 消去存在量词 skolem 函数 化为前束型 把母式化为合取范式 消去全称量词 消去连词符号 更换变量名称,任何文字的析取式称为子句，由子句构成的集合称为子句集。 任何一个谓词公式都可以通过应用等价关系和推理规则化为相应的子句集。,17,常用等价关系,18,常用等价关系,19,(1)消去蕴涵符号,只应用和符号，以AB替换A=B,例如： AB代替(AB) AB代替(AB) ( x)A代替( x)A ( x)A代替( x)A A代替(A),20,(3)对变量标准化,在任一量词辖域内，受该量词约束的变量为一哑元(虚构变量)，它可以在该辖域内处处统一地被另一个没有出现过的任意变量所代替，而不改变公式

9、的真值。合适公式中变量的标准化，意味着对哑元改名以保证每个量词有其自己唯一的哑元。,21,(4)消去存在量词,Skolem函数: 在公式( y)( x)P(x,y)中，存在量词是在全称量词的辖域内，我们允许所存在的x可能依赖于y值。令这种依赖关系明显地由函数g(y)所定义，它把每个y值映射到存在的那个x。这种函数叫做Skolem函数。 如果用Skolem函数代替存在的x,我们就可以消去全部存在量词，并写成： ( y) P(g(y),y) Skolem函数所使用的函数符号必须是新的，即不允许是公式中已经出现过的函数符号。,22,从一个公式消去一个存在量词的一般规则是以一个Skolem函数代替每个

10、出现的存在量词的量化变量，而这个Skolem函数的变量就是由那些全称量词所约束的全称量词量化变量，这些全称量词的辖域包括要被消去的存在量词的辖域在内。 如果要消去的存在量词不在任何一个全称量词的辖域内，那么我们就用不含变量的Skolem函数即常量。例如，( x)P(x)化为P(A)，其中常量符号A用来表示我们知道的存在实体。A必须是个新的常量符号，它未曾在公式中其它地方使用过。 例如：( z)( y)( x)P(x,y,z)被( y)P(g(y),y,A)代替，其中g(y)为一Skolem函数。,23,(5)化为前束形,到这一步，已不留下任何存在量词，而且每个全称量词都有自己的变量。把所有全称

11、量词移到公式的左边，并使每个量词的辖域包括这个量词后面公式的整个部分。所得公式称为前束形。前束形公式由前缀和母式组成，前缀由全称量词串组成，母式由没有量词的公式组成，即 前束形 = (前缀) (母 式) 全称量词串 无量词公式,24,(6)把母式化为合取范式,任何母式都可写成由一些谓词公式和(或)谓词公式的否定的析取的有限集组成的合取。这种母式叫做合取范式。我们可以反复应用分配律。把任一母式化成合取范式。,ABC 化为 ABAC,25,(8)消去连词符号,用(AB),(AC)代替(AB)(AC)，以消去明显的符号。反复代替的结果，最后得到一个有限集，其中每个公式是文字的析取。任一个只由文字的析

12、取构成的合适公式叫做一个子句。,26,化为子句集实例,教材P70,27,消解推理规则,假言推理 合并 重言式 空子句（矛盾） 三段论 常用规则,含有变量的消解式,28,消解推理规则,令L1为任一原子公式，L2为另一原子公式； L1和L2具有相同的谓词符号，但一般具有不同的变量。已知两子句L1和L2,如果L1和L2具有最一般合一者，那么通过消解可以从这两个父辈子句推导出一个新子句 ()。 这个新子句叫做消解式。它是由取这两个子句的析取，然后消去互补对而得到的。,29,从父辈子句求消解式的例子,(a) 假言推理,(c) 重言式,(b) 合并,(a) 假言,30,(d) 链式(三段论),(e) 空子

13、句(矛盾),31,含有变量的消解式,为了对含有变量的子句使用消解规则，我们必须找到一个置换，作用于父辈子句使其含有互补文字。令父辈子句由Li和Mi给出，而且假设这两个子句中的变量已经分离标准化。设li是Li的一个子集，mi是Mi的一个子集，使得集li和mi的并集存在一个最一般的合一者。消解两个子句Li和Mi，得到的新子句: Li-liMi-mi 就是这两个子句的消解式。,32,消解式的多种选择,消解两个子句时，可能有一个以上的消解式，因为有多种选择li和mi的方法。不过，在任何情况下，它们最多具有有限个消解式。,Px,f(A)Px,f(y)Q(y) 和 Pz,f(A)Q(z) 如果取 li=P

14、x,f(A)， mi=Pz,f(A) 那么得到消解式: Pz,f(y)Q(z)Q(y) 如果取 li=Q(y)，mi=Q(z) 那么得到消解式: Px,f(A)Px,f(y)Py,f(A) 进一步消解得消解式为: Py,f(y),可见这两个子句消解一共可得4个不同的消解式，其中3个是消解P得到的，而另一个是由消解Q得到的。,33,对含有变量的子句使用消解的例子,34,消解推理常用规则,35,消解反演求解过程,基本思想 把要解决的问题作为一个要证明的命题，其目标公式被否定并化成子句形，然后添加到命题公式集中去,把消解反演系统应用于联合集，并推导出一个空子句(NIL)，产生一个矛盾，这说明目标公式

15、的否定式不成立，有目标公式成立，定理得证，问题得到解决。即这与数学中反证法的思想十分相似。,36,消解反演,给出一个公式集S和目标公式L，通过反证或反演来求证目标公式L，其步骤如下： 否定L，得到L； 把L添加到S中去； 把新产生的集合L，S化为子句集； 应用消解原理，对子句集进行消解，并把每次消解得到的消解式并入子句集中，如此反复进行，力图推导出一个表示矛盾的空子句，若出现空子句，则停止消解，此时就证明了L为真。 例子 自然数,37,eg1 自然数,有如下事实： F1：自然数都是大于0的整数。 F2：所有整数不是奇数就是偶数。 F3：偶数除以2是整数。 求证：所有自然数不是奇数就是其一半为整

16、数的数。,38,1、用谓词公式的形式表示事实和问题,F1: (x)(N(x) GZ(x) I(x) F2: ( x)(I(x) E(x) O(x) F3: ( x)(E(x) I(f(x) 其中，f(x)x/2 L: ( x)(N(x) O(x) I(f(x),39,2、把L，S化为子句集,1. N(x) GZ(x) 2. N(u) I(u) 3. I(y) E(y) O(y) 4. E(z) I(f(z) 5. N(t) 6. O(v) 7. I(f(w),40,3、对子句集进行消解,反演树,41,消解反演过程的举例,前提：每个储蓄钱的人都获得利息。结论：如果没有利息，那么就没有人去储蓄钱。

17、,42,前提和结论化为下列的子句集,S=S(x,y)M(y)I(f(x),S(x,y)M(y)E(x,f(x)其中，y=f(x)为Skolem函数。而,L I(z),S(a,b),M(b),令S(x,y)表示x储蓄y M(x)表示x是钱 I(x)表示x是利息“ E(x，y)表示x获得y 命题,结论,43,步骤,(1) 否定L，即有 L I(z),S(a,b),M(b) (2) 把 L添加到S中去，即 S=L，S=S(x,y)M(y)I(f(x), S(x,y)M(y)E(x,f(x),I(z),S(a,b),M(b) (3) 把新产生的集合S化成子句集,即 S= S(x,y)M(y)I(f(x

18、), S(x,y)M(y) E(x,f(x),I(z), S(a,b), M(b) (4) 应用消解原理，力图推导出一个表示矛盾的空子句NIL。,44,反演树,S(x,y)M(y)I(f(x) S(x,y)M(y) E(x,f(x) I(z) S(a,b) M(b),45,基于消解反演的问题求解,消解反演除了证明定理之外，还可以用来求解问题，其方法与定理证明类似。 步骤 a）把已知前提用谓词公式表示出来，并化为相应的子句集S； b）把目标公式的否定产生的每个子句添加到目标公式否定之否定的子句中，得到重言式； c）按反演树执行消解，直至根部得到某个子句为止； d）用根部的子句作为一个回答语句,4

19、6,答案求取涉及到把一棵根部有NIL的反演树变换为在根部带有可用作答案的某个语句的一颗证明树。由于变换关系涉及到把由目标公式的否定产生的每个子句变换为一个重言式，所以被变换的证明树就是一棵消解的证明树，其在根部的语句在逻辑上遵循公理加上重言式，因而也单独地遵循公理。因此被变换的证明树本身就证明了求取办法是正确的。,47,例子,“如果无论约翰(John)到哪里去，菲多(Fido)也就去那里，那么如果约翰在学校里，菲多在哪里呢?”,这个问题说明了两个事实，然后提出一个问 题，而问题的答案大概可从这两个事实推导出。这两个事实可以解释为下列公式集S： ( x)AT(JOHN,X)=AT(FIDO,X)

20、和 T(JOHN,SCHOOL),目标公式( x)AT(FIDO,x),子句形式否定为 ( x)AT(FIDO,x),AT(FIDO,x),48,反演树,从消解求取答案的反演树,49,求解,(1) 目标公式否定的子句形式为 :AT(FIDO,x) 把它添加至目标公式的否定之否定的子句中去，得重言式 AT(FIDO,x)AT(FIDO,x) (2) 用反演树进行消解，并在根部得到子句:AT (FIDO，SCHOOL) (3) 从根部求得答案AT(FIDO，SCHOOL)，用此子句作为回答语句。因此，子句 AT (FIDO，SCHOOL)就是这个问题的合适答案，,50,例子,已知F1: 王（wan

21、g）先生是小李（li）的老师。 F2: 小李与小张（zhang）是同班同学。 F3: 若x，y是同班同学，则x的老师也是y 的老师。 求小张的老师是谁？,定义谓词 T(x，y) x是y的老师。 C (x，y) x和y是同班同学。,51,例子（续1）,表示前提 F1: T（wang， li ） F2: C（ li ，zhang） F3: (x)( y)( z)( C (x，y) T（z，x） T（z，y）) 表示问题 (u) T （ u ，zhang） 对问题的否定 (u) T （ u ，zhang）,(u)(T （ u ，zhang）),52,例子（续2）,构造反演树,C （ li ，zhan

22、g）,T （wang，li）,53,例子（续3 构造证明树）,目标公式的否定 化为子句 T （ u ，zhang） 否定之否定 T （ u ，zhang） 构成重言式 T （ u ，zhang） T （ u ，zhang）,问题的答案,54,另一种问题求解的方法,A）把已知前提用谓词公式表示出来，并化为相应的子句集S； B）把目标公式的否定与谓词ANSWER（x）构成一个析取式； C）把此析取式化为子句集， 并入子句集S中，得到S D）对S应用消解原理进行消解，按反演树执行消解，直至根部得到某个子句为止； E）若得到消解式ANSWER，答案就在其中。,Answer是为求解问题而专设的谓词，其变

23、元必须与目标公式的变元完全一致,55,练习,设A,B,C三人中有人从不说真话，也有人从不说假话，某人向这三人提出同一个问题：谁是说谎者？A答：“B和C都是说谎者”；B答：“A和C都是说谎者”； C答：“A和B至少有一个是说谎者”。求谁是老实人？谁是说谎者？,56,解答,首先定义谓词 T（x）表示说真话 表示已知条件 (1)T(A) T(B) T(C) (2) T(A) T(B) T(C) (3) T(B) T(A) T(C) (4) T(B) T(A) T(C) (5) T(C) T(A) T(B) (6) T(C) T(A) T(B),化为子句集 (1) T(A) T(B) (2) T(A)

24、 T(C) (3) T(A) T(B) T(C) (4) T(B) T(C) (5) T(C) T(A) T(B) (6) T(C) T(A) (7) T(C) T(B),57,证明A和B不是老实人,设A不是老实人，则有 T(A)，把它否定得到（8）T(A)，并入S，得到S,并不要求全部子句都用到，一个子句可以多次被使用,58,求解谁是老实人？,把目标公式(x)T(x)的否定 (x)T(x)与ANSWER(x)组成的析取式化为子句（8） T（x） ANSWER(x)，将其加入子句集S得到S,59,练习快乐学生问题,假设任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有的

25、考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。求证：张是快乐的。,先将问题用谓词表示如下：R1:任何通过计算机考试并获奖的人都是快乐的( x)(Pass(x, computer)Win(x, prize)Happy(x)R2:任何肯学习或幸运的人都可以通过所有考试( x)( y)(Study(x)Lucky(x)Pass(x, y)R3:张不肯学习但他是幸运的Study(zhang)Lucky(zhang)R4:任何幸运的人都能获奖( x)(Luck(x)Win(x,prize)结论张是快乐的的否定Happy(zhang),60,将上述谓词公式转化为子句集,首先将每一个表示逻辑条件的谓词

26、子句转换为子句集可以接受的Skolem标准形。 由R1及逻辑转换公式:PWH = （PW） H ，可得 (1) Pass(x, computer)Win(x, prize)Happy(x) 由R2可得(2) Study(y)Pass(y,z) (3) Lucky(u)Pass(u,v) 由R3可得(4) Study(zhang) (5) Lucky(zhang) 由R4可得 (6) Lucky(w)Win(w，prize) 由结论可得(7) Happy(zhang) 结论的否定,61,进行归结,根据以上7条子句，归结如下： (8) Pass(w, computer)Happy(w)Luck(w

27、) 由(1)，(6)归结，w/x (9) Pass(zhang, computer)Lucky(zhang) 由 (8)，(7)归结，zhang/w (10) Pass(zhang, computer) (9)，(5)归结 (11) Lucky(zhang) (10),(3)归结,zhang/u, computer/v (12) (11),(5)归结得到NIL子句,从而证明结论,62,63,例子：猴子摘香蕉问题,64,定义谓词,ON（s） 在状态s下，当猴子在箱子顶上时，谓词ON具有真值T AT（box，x，s） 在状态s下，箱子位于x位置 AT（monkey，x，s） 在状态s下，猴子位于x

28、位置 HB（s） 在状态s下，当猴子摘到香蕉时，谓词HB具有真值T,65,算符的意义,把一种状态映射为另一种状态的函数 grasp(s)的值是当算符grasp作用于状态s时得到的新状态 (s)(ON(s) AT(box, c, s) HB(grasp(s) 首先得到合取(s) W（ s）的一个证明，然后采用答案求取过程得到解答 此回答语句将包含一个以算符函数的组合形式表示的目标状态表达式,66,问题的表示,已知： 1, ON(s0) 2, (x)(s)(ON(s) AT(box, x, push(x, s) 3, (s)(ON(climb(s) 4, (s)(ON(s) AT(box, c,

29、s) HB(grasp(s) 5, (x)(s)(AT(box, x, s) AT(box, x, climb(s) 求解：(s)HB(s),67,问题的子句集,1, ON(s0) 2, ON(s1) AT(box, x1, push(x1, s1) 3, ON(climb(s2) 4, ON(s3) AT(box, c, s3) HB(grasp(s3) 5, AT(box, x4, s4) AT(box, x4, climb(s4) 6, HB(s5),68,HB(s5),ON(s3) AT(box, c, s3) HB(grasp(s3),ON(s3) AT(box, c, s3),ON(climb(s2),AT(box, c, climb(s2),ON(s0),ON(s1) AT(box, x1, push(x1, s1),AT(box, x1, push(x1, s0),AT(box, x4, s4) AT(box, x4, climb(s4),AT(box, x4, climb(push(x4,s0),NIL,反演证明树,69,HB(s5) ,HB(grasp(s3) , HB(grasp(climb(s2),HB(grasp(climb(push(c,s0),反演求解树,70,