三章谓词演算与消解归结原理.ppt

《三章谓词演算与消解归结原理.ppt》由会员分享，可在线阅读，更多相关《三章谓词演算与消解归结原理.ppt（79页珍藏版）》请在三一文库上搜索。

1、第三章 谓词演算与消解(归结)原理,命题演算 谓词演算 推理规则产生谓词演算表达式 应用 归结原理,3.1 命题演算,3.1.1 符号和命题,命题演算的符号：是命题符号,命题符号代表命题，是关于现实世界的能分辨真假值的陈述句。 命题符号：P，Q，R，S，T,命题演算的符号： 真值符号：True, false 联结词：，=， 通过联结词可把多个命题组成合成的命题，也称为合式公式。,3.1.2 命题演算的语义,3.1 命题演算,如两个命题表达式 在任何真值指派下都有相同的值，则称为是等价的 （P 29 ）表2.2所示的真值表证明： P=Q 与 P Q 等价。 对于命题表达式 P，Q，R (P)=P

2、 ; (PQ) (P=Q),否定律： (PQ) (PQ) (PQ) (PQ) 分配律：P(QR) (PQ)(PR) 分配律：P(QR)(PQ)(PR) 交换律：(PQ) (QP) 交换律：(PQ) (QP) 结合律：(PQ)R) (P(QR) 结合律：(PQ)R) (P(QR) 置换律：(P=Q) (Q=P),3.1 命题演算,3.2 谓词演算,命题演算中，P，Q代表一定的命题，如： P：星期四下雨 而谓词：Weather（X，Y）代表日期与天气的关系 Weather（Tuesday，Rain）,可以操纵命题演算表达式 允许包含变元 Weather（X，Rain）,3.2.1 谓词的语法和命题

3、,3.2 谓词演算,谓词演算的字母表组成： （1）英文字母组合，包括大写与小写 （2）数字集合0,1,9 （3）下划线 如：George fires bill xxxx,谓词演算符号包括： 1.真值符号 true 和 false。 2.常元符号,第一个字符为小写字母的符号表达式。 3.变元符号,第一个字符为大写字母的符号表达式。 4.函词符号,第一个字符为小写字母的符号表达式, 函词有一个元数, 指出从定义域中映射到值域中的每个元素。,3.2 谓词演算,例： likes (george, kate). likes (X, george). likes (george, susie). like

4、s (X, X). likes (george, sarah, tuesday). friends (bill, richard). friends (bill, george). friends (father (david), father (andrew) helps (bill, george). helps (richard, bill).,3.2 谓词演算,原子命题：是一个n元谓词，后跟n个项，用括号括起来 并用逗号分开。,常元符号,项,3.2.1 谓词的语法和命题,与谓词相关的一个正整数称为元数或“参数数目”，具有相同的名但元数不同的谓词是不同的。 真值true和false也是原

5、子命题。 任何原子命题都能够用逻辑操作符将其变成谓词演算的命题。用的联结词也和命题演算一样: , , = 和。 当一个变元在一个命题中作为参数出现时,它代表的是域中不特定的对象。谓词演算包括两个符号, 量词（全称量词）和彐（存在量词）, 用于限定包含变元的命题的含义。,3.2.1 谓词的语法和命题,一个量词后面紧跟着一个变元和一个命题。例如： X likes (X, ice_cream). 彐Y friends (Y, peter).,全称量词 , 表明命题对于变元的变域中的所有的值都为真。 存在量词彐, 表明该命题对于变元的变域中的一些值为真。,例：命题,3.2.1 谓词的语法和命题,plu

6、s(two,three) equal(plus(two,three) 彐xfoo(x,two,plus(two,three) equal(plus(two,three),five),3.2.2 谓词演算的语义,谓词演算的语义提供了确定合式表达式真值的形式基础。表达式的真值依赖于常元、变元、谓词、函词到论域中的映射，在论域中的关系的真假决定了相应表达式的真假。 例如：,friends ( george, susie ) friends ( george, kate ),3.2.2 谓词演算的语义,一个论域D上的解释： 假设论域D是一个非空集合，在D上的一个解释把论域D的实体指派给一个谓词演算表达

7、式的每一个常元、变元、谓词及函词符号，于是有： 1）每一个常元指派了D的一个元素。 2）对每一个变元，指派D的一个非空集合，这是该变元的变域。 3）每个n元谓词P定义在论域D中的n个参数上，并定义了从Dn到T，F的一个映射。 4) 每个m元函词f定义在论域D的m个参数上，并定义了从Dm到T，F的一个映射。 在一种解释下，一个表达式的意义是在该解释下的一个真值指派。,3.2.2 谓词演算的语义,谓词演算表达式的真值 设有表达式E和在非空论域D上对E的一个解释I，E的真值按以下规律决定： 1）一个常元的值是根据I指派给它的D的一个元素。 2）一个变元的值是根据I指派给它的D的一个元素集合。 3）一

8、个函词的值是根据由I指派给它的参数值计算得到的D的元素。 4）真值符号true的值是T，false的值是F。 5）原子命题的值或者为T，或者为F，取决于解释I。 6）如果一个命题的值为F，则其否定式为T，否则为F。 7）如果 11)如果对于在解释I下的X的每一个指派，S的值为T，则 X S为T，否则为F。 12）如果在解释I下存在X的一个指派使得S的值为T，则彐X S为T，否则为F。,3.2.2 谓词演算的语义,变元：likes(george,X) 这个变元名可以由任何其他变元名代替，不会改变表达式的意思。,变元的量词约束是谓词演算语义的重要部分 在谓词演算中,变元有两种约束使用的方法: 在特

9、定解释下,命题对变元的变域中的所有常元指派为真,则称该变元是全称性变元。代表全称量词的符号是 ,括号常常用于表示量词的约束范围 存在性变元。至少存在变元的变域中的一个值使包含变元的表达式为真时，表达式才为真。代表存在量词的符号是彐,3.2.2 谓词演算的语义,否定与全称量词、存在量词之间的关系 。 对于谓词 P, Q, 变元 X, Y有： 彐X P(X) X P(X) X P(X) 彐X P(X) 彐X P(X) 彐Y P(Y) X Q(X) Y Q(Y) X (P(X)Q(X) ) X P(X) Y Q(Y) 彐X (P(X)Q(X) ) 彐X P(X)彐Y Q(Y),3.3 推理规则产生谓

10、词演算表达式,3.3.1 推理规则 推理规则：实际上是一个从其他谓词演算命题产生新的谓词演算命题的机械方法。亦即推理规则产生基于给定逻辑断言的句法形式的新命题。当每个由逻辑表达式集S上的推理规则产生的命题X都是S的逻辑结果,则称该逻辑规则是合理的。,S: X human(X) = mortal(X). human(Socrates). X: mortal (Socrates).,假言推理和消解原理都是合理的推理规则的例子。,假言推理：如果命题P，P = Q为真，应用假言推理得出Q为真。,S: X human(X) = mortal(X). human(Socrates). X: mortal

11、(Socrates).,human(Socrates) = mortal(Socrates),合一 算法,3.3.2 合一,伪代码写的函数 Unify 用于计算两个谓词表达式的最一般合一,是判断两个谓词表达式匹配所需的一种代入算法 合一表明了两个或多个表达式在什么条件下可以称为等价的。,以两个谓词演算表达式为参数,若这两个表达式可以合一, 则返回最一般合一代入,否则返回 FAIL。,3.3.2 合一,function unify (E1, E2) ; begin case end %end case end,首先,它递归地试图对表达式的初始成分合一。如果成功, 这次合一返回的任何代入式被用到两

12、个表达式的剩下部分, 然后以这两个表达式为参数。 终止条件是两个参数之一为一个符号 (谓词名, 函词名, 变元, 常元 ), 或两个表达式的每一元素都已匹配了。,3.3.2 合一,case E1, E2 或者是常元或者是空表: %递归终止。 If E1 E2 then return else return FAIL; E1是一个变元: if E1在E2中出现 then return FAIL else return E2/E1; E2是一个变元: if E2在E1中出现 then return FAIL else return E1/E2; 其他情况: % E1和E2都是表,3.3.2 合一,

13、begin HE1:= E1的第一个元素; HE2:= E2的第一个元素; SUBS1:= unify (HE1, HE2); if SUBS1 FAIL then return FAIL TE1:= apply (SUBS1, E1的后半部) TE2:= apply (SUBS1, E2的后半部) SUBS2:= unify (TE1, TE2 ), if SUBS2 FAIL then return FAIL else return SUBS1与SUBS2 的合成 end,3.3.3 合一的一个例子,通过以下调用来跟踪算法的运行过程： unify (parents X (father X)

14、 (mother bill), (parents bill (father bill) Y ) 第一次调用: unify (parents, parents) 这次调用成功, 返回代入集 。 第二次调用: unify (X, bill) 这次调用成功,返回代入 bill / X 。,3.3.3 合一的一个例子,在此基础上又调用: unify (father bill) (mother bill), (father bill) Y ) 导致调用: (1) unify(father bill),(father bill) unify (father, father) unify (bill, bi

15、ll) unify ( ), ( ) 所有的调用都成功,返回空代入集 。 (2) unify (mother bill), Y),3.4 应用 :一个基于逻辑的金融投资辅助决策程序,一位有三个人需赡养,有$22000存款,每年有$25000的稳定收入的投资者的情况,可产生一个由下列命题组成的逻辑系统: 1.savings (inadequate) = investment (savings). 2.savings (adequate)income (adequate ) = investment (stocks). 3. Savings (adequate)income (inadequate

16、) = investment (combination). 4. X amountsaved (X)彐Y(dependents (Y) greater (X, minsavings (Y) = savings (adequate). 5. X amountsaved (X) 彐Y (dependents (Y) greater (X, minsavings (Y) = savings (inadequate).,3.4 应用,6. X earnings (X, steady) 彐Y (dependents (Y) greater (X, minincome(Y) = income (adequ

17、ate). 7. X earnings (X, steady)彐Y (dependents (Y) greater (X, minincome (Y) = income (inadequate). 8. X earnings (X, unsteady) = income (inadequate). 9. amountsaved (22000). 10. earnings (25000, steady). 11. dependents (3).,其中: minsavings (X) = 5000 * X; minincome (X) = 15000 + (4000 * X),3.4 应用,第一步

18、把第10、11与第7的前提合一, 得: 12. Income (inadequate) .,第二步把第9、11与第4的前提合一,得: 13. savings (adequate),将第12、13条命题检验第3条命题得到其前提为真。于是运用假言推理后得到结论: investment (combination), 这就是给投资者的建议。,(存款的人应该把他们多余的钱分别用于存款和买股票，在增加存款做保险的同时试图通过做股票以增加收入。),3.5 消解定理证明,消解是一种应用于谓词演算中的定理证明技术，是人工智能问题求解的一个组成部分。消解描述了如何用最少的合一次数在一个子句数据库中发现矛盾的方法。

19、,具体方法如下： 对所要证明的命题取反，把它加到已知为真的公理集中，然后用消解推理规则证明这将导致一个矛盾，一旦证明了否定目标与已知公理集不一致，就能推导出原来的目标与已知公理集是一致的，从而定理得证。,3.5 消解定理证明,3.5.1 引言 消解否证包含以下步骤： 把前提或公理转换成子句形式。 把求证目标的否定的子句形式加到公理集合中。 对所有这些子句进行消解，产生它们的逻辑结果子句。 用产生空子句的方法来得出矛盾。 否定目标的否证在用于产生空子句的代换下为真。,3.5.1 引言,消解否证需要所有公理和否定目标为子句形式,子句形式把一个逻辑数据库表示为一个文字析取式的集合。一个文字是一个原子

20、表达式或原子表达式的否定。,消解作用于两个子句, 其中一个包含某文字,另一个包含该文字的否定,如果这些文字包含变元,必须用合一使它们相等。 一个新的子句就此产生了,它包含两个子句中所有谓词的析取,除了该文字和它的否定以外。,3.5.1 引言,用消解所做的等价的推理把以下谓词演算公式变换成子句形式 ： 谓词形式 子句形式 1.All dogs are animals (X) (dog (X) animal (X) dog (X) animal (X) 2.Fido is a dog dog ( fido ) dog ( fido ) 3.all animals will die (Y) (ani

21、mal (Y) die (Y) animal (Y) die (Y),证明：fido will die,对目标“取反” ：, die ( fido ),dog(X) animal(X). animal(Y) die(Y). Y/X dog(fido). dog(Y) die(Y). fido/Y die(fido). die(fido). 图 “死狗”问题消解证明,3.5.1 引言,3.5.2 为消解否证产生子句形式,本节提出一个由一系列变换组成的算法，这些变换可以把任何谓词演算表达式归约为子句形式，在此过程中保持其真值、一般性和不可满足性不变。,即如果在原谓词演算表达式中存在一个矛盾，则其子

22、句形式中也存在一个矛盾，变换不牺牲消解否证的完备性。,3.5.2 为消解否证产生子句形式,设X,Y,Z,W表示变元；l,m,n表示常元；a,b,c,d,e表示谓词名。要归纳为子句的表达式： 1.( X) (a(X)b(X) c(X, l )(彐Y) (彐Z)c(Y，Z)d(X,Y) ) ) ( X) (e(X),2.( X) ( a(X) b(X)c(X，l)(彐y) (彐Z)c(Y,Z)d(X,Y)( ）(e(X)）,3.( X) ( a(X) b(X)c(X, l)(彐Y) ( Z) c(Y,Z)d(X,Y)( X)(e(X),4.( X) ( a(X) b(X)c(X, l ) (彐Y)

23、 ( Z) c(Y,Z)d(X,Y)( W) (e(W),5.( X)(彐Y)( Z)( W) ( a(X) b(X)c(X,l) c(Y,Z)d(X,Y)e(W),3.5.2 为消解否证产生子句形式,斯柯伦标准化：去掉所有的存在量词,彐Z（foo(Y，Z),foo(Y，k),斯柯伦常元,如果谓词中含有多个参数，而彐约束变元在约束变元的约束范围内，则彐约束变元必须是那些其他变元的函数。,如： （X）(彐Y)(mother(X,Y),3.5.2 为消解否证产生子句形式,6. ( X)( Z)( W) ( a(X) b(X)c(X,l) c (f(X),Z)d(X,f(X)e(W),5.( X)(

24、彐Y)( Z)( W) ( a(X) b(X)c(X,l) c(Y,Z)d(X,Y)e(W),7.( a(X) b(X)c(X, l)( c(f(X), Z)d(X, f(X)e(W),8. a(X) b(X)c(X,l)e(W) a(X) b(X) c(f(X), Z)d(X, f(X)e(W),9a: a(X) b(X)c(X,l)e(W) 9b: a(X) b(X) c(f(X), Z)d(X, f(X)e(W),10a: a(X) b(X)c(X,l)e(W) 10b: a(U) b(U) c(f(U), Z) d(U, f(U)e(V),3.5.3 消解证明过程,例1: “幸运学生”

25、的故事: “任何通过了历史考试并中了彩票的人是快乐的。任何肯学习或幸运的人可以通过所有考试, John不学习但很幸运,任何人只要是幸运的就能中彩。John快乐吗?“,1. 第一步把这些句子变成谓词形式:,定义一些函词： pass(x,y) , win(x, lottery) , happy(x) , study(X), lucky(x),3.5.3 消解证明过程,“任何通过了历史考试并中了彩票的人是快乐的。任何肯学习或幸运的人可以通过所有考试, John不学习但很幸运,任何人只要是幸运的就能中彩。John快乐吗?“, X (pass (X, history)win (X, lottery) h

26、appy (X) ) X Y ( study (X)lucky (X) pass (X,Y) ) study (john) lucky (john) X (lucky (X)win (X, lottery) ),3.5.3 消解证明过程,1. pass (X, history)win (X, lottery)happy (X) 2. study (Y)pass (Y, Z) 3. lucky (V)pass (V,W) 4. study (john) 5.lucky (john) 6. lucky (U)win (U, lottery), X (pass (X, history)win (X,

27、 lottery) happy (X) ) X Y ( study (X)lucky (X) pass (X,Y) ) study (john) lucky (john) X (lucky (X)win (X, lottery) ),将这四个谓词演算命题转换成子句形式:,3.5.3 消解证明过程, pass(X,history) win(U,lottery) lucky(U) win(X,lottery)happy(X) U/X pass(U,history) happy(john). happy(U) lucky(U). john/U lucky(john). pass(john,histo

28、ry) lucky(john). pass(john,history). lucky()pass(V,W). john/V,history/W lucky(john). lucky(john). 图 “快乐学生”问题的消解否证,子句 1,子句 6,子句 7,子句 5,子句 3,子句 5,子句集及其化简,子句和子句集： 定义3.14 原子谓词公式及其否定统称为文字。 定义3.15 任何文字的析取式称为子句。 定义3.16 不含任何文字的子句称为空子句。 由于空子句不含有任何文字，也就不能被任何解释所满足，因此空子句是永假的，不可满足的。 空子句一般被记为或NIL。 定义3.17 由子句或空子句所

29、构成的集合称为子句集。,在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理规则化成相应的子句集。,( X) (a(X)b(X) c(X, l )(彐Y) (彐Z)c(Y，Z)d(X,Y) ) ) ( X) (e(X),其化简步骤如下： 消去连接词“”和“” 减少否定符号的辖域 对变元标准化 化为前束范式 消去存在量词 化为Skolem标准形 消去全称量词 消去合取词 更换变量名称,在上述化简过程中，由于在消去存在量词时所用的Skolem函数可以不同，因此化简后的标准子句集是 不唯一的。 这样，当原谓词公式为非永假时，它与其标准子句集并不等价。但当原谓词公式为永假（或不可满足）时，其标准

30、子句集则一定是永假的，即Skolem化并不影响原谓词公式的永假性。 这个结论很重要，是归结原理的主要依据，可用定理的形式来描述。,归结原理基本思想: 首先把欲证明问题的结论否定，并加入子句集，得到一个扩充的子句集S。然后设法检验子句集S是否含有空子句，若含有空子句，则表明S是不可满足的；若不含有空子句，则继续使用归结法，在子句集中选择合适的子句进行归结，直至导出空子句或不能继续归结为止。 归结原理包括: 命题逻辑归结原理 谓词逻辑归结原理,例3.9 设C1 =P Q ，C2=Q，C3=P，求C1、C2、C3的归结式C123。,简单的例子：,解：（1）若先对C1、C2归结,（2）若先对C1、C3

31、归结,归结树,如果改变归结顺序，同样可以得到相同的结果： 即其归结过程是不唯一的。,3.5.3 归结证明过程,例2： 假设: “所有不贫穷并且聪明的人是快乐的。那些看书的人是不笨的。John能看书并且富有。快乐的人过着激动人心的生活。你能发现谁过着激动人心的生活吗?“,把上述故事翻译成谓词演算表达式: X( poor(X)smart(X)happy(X) Y( read(Y)smart(Y) read(john) poor(john) Z( happy(Z)exciting(Z),否定目标是： 彐 W(exciting(W),3.5.3 归结证明过程,1.poor(X) smart(X)hap

32、py(X) 2. read(Y)smart(Y) 3.read(john) 4. poor(john) 5. happy(Z)exciting(Z) 6. exciting(W),X( poor(X)smart(X)happy(X) Y( read(Y)smart(Y) read(john) poor(john) Z( happy(Z)exciting(Z) 彐 W(exciting(W),3.5.3 归结证明过程, exciting(W) happy(Z)exciting(Z) Z/W happy(Z) poor(X) smart(X)happy(X) X/Z poor(X)smart(X)

33、 read(Y)smart(Y) Y/X poor(Y) read(Y) poor(john),子句 6,子句 5,子句 1,子句 2,这个例子的消解否证如图所示：,john/Y, read(john),read(john),子句 4,子句 3,3.5.3 归结证明过程, exciting(W) happy(Z)exciting(Z) Z/W happy(Z) poor(X) smart(X)happy(X) X/Z poor(X)smart(X) read(Y)smart(Y) Y/X poor(Y) read(Y) poor(john) john/Y, read(john),read(jo

34、hn), exciting(W) happy(Z)exciting(Z) Z/W happy(Z) poor(X) smart(X)happy(X) X/Z poor(X)smart(X) read(Y)smart(Y) Y/X poor(Y) read(Y) poor(john) john/Y,从归结否证中提取答案,3.6 用归结法求更为复杂问题例子,例1：某记者到一孤岛采访，遇到了一个难题，即岛上有许多人说假话，因而难以保证新闻报道的正确性，不过有一点他是清楚的，这个岛上的人有一特点：说假话的人从来不说真话，说真话的人也从来不说假话。一次记者遇到了孤岛上的三个人，为了弄清楚谁说真话，谁说假

35、话，他向这三个人中的每一个都提了一个同样的问题，即 “谁是说谎者？” 结果A答“B和C都是说谎者”， B答“A和C都是说谎者”， C答“A和B中至少有一个 是说谎者”， 试问记者如何从回答中理出头绪。,3.6 用归结法求更为复杂问题例子,以A，B，C三个命题来表示A，B，C三个是老实人（不说谎）,A答“B和C都是说谎者” B答“A和C都是说谎者” C答“A和B中至少有一个 是说谎者”,如果A说真话，则B和C一定说谎，因此有：A B C 如果A说假话，则B和C中至少有一人说真话,因此有: A B C 以同样的推理方式可得到： 如果B说真话, 如果B说假话 B A C B A C 如果C说真话,

36、如果C说假话 C A B C A B,3.6 用归结法求更为复杂问题例子,对以上蕴含式加以推理,并化成子句形式,可得： A B （1） A C （2） A B C （3） B C （4） A B C （5） A C （6） B C （7）,3.6 用归结法求更为复杂问题例子,（1）和（7）归结，得： A C （8） （2）和（8）归结，得： A （9） （6）和（9）归结，得： C （10） （4）和（10）归结，得： B （11）,说明？ 谁是说谎者？,A和B都是说谎者，而C是老实人,3.6 用归结法求更为复杂问题例子,例2: 四对夫妇中，王结婚时，周送了礼；周和钱是同一排球队的队员；李的爱

37、人是陈的爱人的表哥；陈夫妇与邻居吵架，徐、周、吴的爱人都去助战；李、徐、周结婚前住一间宿舍，试用归结法求王、周、钱、陈、李、徐、吴、孙八人谁是男？谁是女？谁和谁是夫妇？,（1）女（李） （2）女（李） 女（徐）即：NOT 女（李） 女（徐） （3）女（李） 女（周）即：NOT 女（李） 女（周） （4）女（周） 女（钱）即：NOT 女（周） 女（钱） （5）女（李） 女（徐） 女（周） 女（钱） 男（王） 男（陈） 男（吴） 男（孙）,则可解得男的是：王、陈、吴、孙 则可解得女的是：李、徐、周、钱,（ 6） couple（王，周） （ 7） couple （陈，李） （ 8） couple （

38、陈，徐） （ 9） couple （陈，周） （10） couple （吴，周） （11） couple （吴，徐） （12） couple （X，Y）男（X）女(Y） （13） couple （陈，李）夫妻（陈，徐） 夫妻（陈，周）夫妻（陈，钱）,例2: 四对夫妇中，王结婚时，周送了礼；周和钱是同一排球队的队员；李的爱人是陈的爱人的表哥；陈夫妇与邻居吵架，徐、周、吴的爱人都去助战；李、徐、周结婚前住一间宿舍，试用消解法求王、周、钱、陈、李、徐、吴、孙八人谁是男？谁是女？谁和谁是夫妇？,男：王、陈、吴、孙 女：李、徐、周、钱,（14）couple（陈，钱） (13)(7)(8)(9)归结; （

39、15）couple(吴,周) couple(吴,徐) couple(吴,李) （16）couple (吴,李) （15）（10）（11）进行归结; （17） couple （王，周） couple （王，徐） （18） couple （王，徐） （17）与（6）归结 （19） couple （孙，周）,3.6 用归结法求更为复杂问题例子,例3: 某村农民王某被害，有四个嫌疑犯A，B，C，D，公安局派出五个侦察员，他们带回的信息各不一样，甲说A，B中至少有一人作案，乙说B ，C中至少有一人作案，丙说C，D中至少有一人作案，丁说A，C中至少有一人与此案无关，戊说B ，D中至少有一人与此案无关，如果

40、这五个侦察员的话都是可靠的，试用消解法求出谁是罪犯。,3.6 用归结法求更为复杂问题例子,（1） A B （2） B C （3）C D （4） A C （5） B D （6） B C （1）、（4）归结； （7） B是罪犯。 （2）、（6）归结； （8）C D （2）、（5）归结； （9） C是罪犯。 （3）、（8）归结。,3.7 归结演绎推理的归结策略 -广度优先策略,广度优先是一种穷尽子句比较的复杂搜索方法。 设初始子句集为S0，广度优先策略的归结过程可描述如下： (1) 从S0出发，对S0中的全部子句作所有可能的归结，得到第一层归结式，把这些归结式的集合记为S1; (2) 用S0中的子句

41、与S1中的子句进行所有可能的归结，得到第二层归结式，把这些归结式的集合记为S2; (3) 用S0和S1中的子句与S2中的子句进行所有可能的归结，得到第三层归结式，把这些归结式的集合记为S3; 如此继续，知道得出空子句或不能再继续归结为止。,例3.19 设有如下子句集： S=I(x)R(x), I(a), R(y)L(y), L(a) 用宽度优先策略证明S为不可满足。 宽度优先策略的归结树如下：,宽度优先策略归结出了许多无用的子句，既浪费时间，又浪费空间。 但是，这种策略有一个有趣的特性，就是当问题有解时保证能找到最短归结路径。 它是一种完备的归结策略。 宽度优先对大问题的归结容易产生组合爆炸，

42、但对小问题却仍是一种比较好的归结策略。,3.7 归结演绎推理的归结策略 -广度优先策略,支持集策略是沃斯(Wos)等人在1965年提出的一种归结策略。 它要求每一次参加归结的两个亲本子句中，至少应该有一个是由目标公式的否定所得到的子句或它们的后裔。 可以证明支持集策略是完备的，即当子句集为不可满足时，则由支持集策略一定能够归结出一个空子句。 也可以把支持集策略看成是在宽度优先策略中引入了某种限制条件，这种限制条件代表一种启发信息，因而有较高的效率,3.7 归结演绎推理的归结策略 -支持集策略,例3.20 设有如下子句集： S=I(x)R(x), I(a), R(y)L(y), L(a) 其中，

43、I(x)R(x)为目标公式的否定。用支持集策略证明S为不可满足。,各级归结式数目要比宽度优先策略生成的少 但在第二级还没有空子句。就是说这种策略限制了子句集元素的剧增，但会增加空子句所在的深度。 支持集策略具有逆向推理的含义，由于进行归结的亲本子句中至少有一个与目标子句有关，因此推理过程可以看作是沿目标、子目标的方向前进的。,3.7 归结演绎推理的归结策略 -支持集策略,主要想法是：归结过程在寻找可归结子句时，子句集中的子句越多，需要付出的代价就会越大。如果在归结时能把子句集中无用的子句删除掉，这就会缩小搜索范围，减少比较次数，从而提高归结效率。 常用的删除方法有以下几种： 纯文字 重言式 包

44、孕,3.7 归结演绎推理的归结策略 -删除策略,纯文字删除法： 如果某文字L在子句集中不存在可与其互补的文字L，则称该文字为纯文字。 在归结过程中，纯文字不可能被消除，用包含纯文字的子句进行归结也不可能得到空子句，因此对包含纯文字的子句进行归结是没有意义的，应该把它从子句集中删除。 对子句集而言，删除包含纯文字的子句，是不影响其不可满足性的。例如，对子句集 S=PQR, QR, Q, R 其中P是纯文字，因此可以将子句PQR从子句集S中删除。,3.7 归结演绎推理的归结策略 -删除策略,重言式删除法 如果一个子句中包含有互补的文字对，则称该子句为重言式。例如 P(x)P(x), P(x)Q(x

45、)P(x) 都是重言式，不管P(x)的真值为真还是为假，P(x)P(x)和P(x)Q(x)P(x)都均为真。 重言式是真值为真的子句。对一个子句集来说，不管是增加还是删除一个真值为真的子句，都不会影响该子句集的不可满足性。因此，可从子句集中删去重言式。,3.7 归结演绎推理的归结策略 -删除策略,包孕删除法 设有子句C1和C2，如果存在一个置换，使得C1C2，则称C1包孕于C2。例如 P(x) 包孕于 P(y)Q(z) =x/y P(x) 包孕于 P(a) =a/x P(x) 包孕于 P(a)Q(z) =a/x P(x) Q(a) 包孕于 P(f(a)Q(a)R(y) =f(a)/x P(x) Q(y) 包孕于 P(a)Q(u)R(w) =a/x, u/y 对子句集来说，把其中包孕的子句删去后，不会影响该子句集的不可满足性。因此，可从子句集中删除哪些包孕的子句。,3.7 归结演绎推理的归结策略 -删除策略,如果一个子句只包含一个文字，则称此子句为单文字子句。单文字子句策略是对支持集策略的进一步改进，它要求每次参加归结的两个亲本子句中至少有一个子句是