RGZN_5谓词逻辑

1、第五章 基于谓词逻辑的机器推理在许多应用中，被编码进入产生式系统数据库的信息来源于说明语句，这些语句难以或者不能自然地用像数组或集合那样的简单结构来表示。例如，机器人求解问题要求具有表达、检索和变换语句集合的能力。而逻辑语句，或者更具体地说，一阶谓词演算能用来表示种类众多的语句,且能给出一种从旧知识直接求得新知识的有效方法数学演绎。即如能证明一个新语句是从那些已知正确的语句导出的，那么我们就可断定这个新语句也是正确的。证明的概念 推广(把演绎包括在内)用来作为一种求取问题的方法。第一节 谓词演算5.1.1 命题逻辑及其局限性 命题 具有真假意义的一句话人们研究用命题逻辑作为一种表达知识的方法，

2、因为它处理简单，并存在一个判定方法。如:可把客观世界的各种事实表示为逻辑命题，用命题逻辑把各种命题写成合适公式（WFF）。例如：雨天 表示为: RAINING 晴天 表示为: SUNNY 雾天 表示为: FOGGY 若为雨天，则非晴天。 表示为： RAININGSUNNY但是，我们很快就会遇到命题逻辑的局限性。假定我们要表示由下列句子叙述的明显事实： 李明是个工人可写为 LIWORKER如果我们也要表示： 王华也是个工人就必须写出 WANGWORKER这是一些完全独立的格式，我们无法从中得出有关李（LI）和王（WANG）相似性的结论。 如果把这些事实表示为如下形式： WORKER（LI） WO

3、RKER（WANG）那么这就要好得多，因为这种表达结构反映出知识本身的结构。如果我们试图用命题逻辑来表示下列句子： 所有的人都会死。那么我们将面临更大的困难，因为如果我们不对问题进行量化，那么我们就必须一个一个地写出某某某会命题逻辑局限性:l 不区分知识的结构与成分;l 不可对问题进行量化而谓词逻辑允许我们表达那些无法用命题逻辑相应地加以表达的事情,可进行演绎,可使用变量及量词( 、彐)。(x)(H(x) D(x)对任意x ,只要x是人 ,则x必然会死。5.1.2 谓词逻辑的句法和语义 基本组成部分: 谓词符号、变量符号、函数符号和常量符号，并用圆括弧、方括弧、花括弧和逗号隔开，以表示论域内的

4、关系。 个体（客体）名称集合（或称论域）D 常量符号： 代表D中某一个确定个体 变量符号： 代表D中任一个个体（客体） 函数符号： f(x1,.,xn)它为Dn D 的一个映射（最终值D） 表达个体之间的对应关系，例如：我们用father(x)表示x的父亲。约定：小写字母f,g,h等表示函数符号，小写字母x,y,z,u,v,w等表示个体变量(变元)符号，小写字母a,b,c等表示个体常量(常元)符号 谓词符号： 由大写字母（单词）表示，定义域为Dn ，值域为T，F 的函数的函数名 项： 常量符号、变量符号、函数符号，（最终值D） 原子谓词公式： P(t1,.,tm) 谓词符号 项 如： P(x,

5、y,z) 命 题 ？ 变量 定义P关系：令P(x,y,z)表示x在y与z之间 命题 ？ 代入确定个体（实例化）：如令x,y,z代表北京、保定、石家庄， 则P(x,y,z)为命题。5.1.3 连词和量词合适公式（WFF）： 通过使用连词（非）、（与）、（或）、=>（ 蕴涵，或隐含）以及 、彐等将原子谓词公式按一定的语法格式连接而成的式子。连词用来表示复合句子。例如，句子“我喜爱音乐和绘画”可写成： LIKE(I，MUSIC)LIKE(I，PAINTING)又如“李住在一幢黄色的房子里”，即可用 LIVES(LI，HOUSE-1)COLOR(HOUSE-1，YELLOW)其中谓词LIVES表

6、示人与物体（房子）间的关系，而谓词COLOR则表示物体与其颜色之间的关系。合取： 用连词把几个（原子）公式连接起来而构成的公式此合取式的每个组成部分叫做合取项连词用来表示可兼有的“或”。例如，句子“李明打蓝球或踢足球”可表示为：PLAYS（LIMING，BASKETBALL）PLAYS（LIMING，FOOTBAL）析取： 用连词把几个公式连接起来所构成的公式此析取式的每一组成部分叫做析取项 合取和析取的真值由其组成部分的真值决定。连词 =>用来表示“如果-那么”的词句。如句子“如果该书是何平的，那么它是蓝色（封面）的”可表示为：OWNS(HEPING，BOOK-1) => COL

7、OR(BOOK-1，BLUE)又如，句子“如果刘华跑得最快，那么他取得冠军”可表示为： RUNS(LIUHUA，FASTEST) => WINS(LIUHUA，CHAMPION)用连词=>连接两个公式所构成的公式叫做蕴涵。蕴涵的左式叫做前项，右式叫做后项。如果前项和后项都是合适公式，那么蕴涵也是合适公式。如果后项取值T（不管其前项的真值如何），或者前项取值F(不管后项的真值如何)，则蕴涵取值T；否则，蕴涵取值F。符号（非）用来否定一个公式的真值，也就是说，把一个合适公式的取值从T变为F，或从F变为T。例如，子句“机器人不在2号房间内”可表示为：INROOM（ROBOT，r2）前面具

8、有符号的公式叫做否定。 如果我们把句子限制为我们至今已介绍过的造句法所能表示的那些句子，而且也不使用变量项，那么我们可以把这个谓词演算的子集叫做命题演算。命题演算对于许多简化了的定义域来说，是一种有效的表示，但它缺乏用有效的方法来表达多个命题（如“所有的机器人都是灰色的”）的能力。要扩大命题演算的能力，我们需要使公式中的命题带有变量。、彐 有时，一个原子公式如P（x），对于所有可能的变量x都具有值T。这个特性可由在P（x）前面加上全称量词（x）来表示。如果至少有一个x值可使P（x）具有值T，那么这一特性可由在P（x）前面加上存在量词（彐x）来表示。例如，句子“所有的机器人都是灰色的”可表示为：

9、 （x）ROBOT（x）COLOR（x，GRAY）而句子“1号房间内有个物体”可表示为: （彐x）INROOM（x，r1）x: 经过量化了的约束变量： 如果一个合适公式中某个变量是经过量化的，我们就把这个变量叫约束变量，否则就叫它为自由变量。句子： 在合适公式中，若所有变量都是受约束的。这样的合适公式叫做句子。 值得指出的是，本书中所用到的谓词演算为一阶谓词演算。不允许对谓词符号或函数符号进行量化。例如，在一阶谓词演算中，（P）P（A）就不是合适公式。又例：每个有理数都是实数有些实数是有理数并非每个实数都是有理数解： 令 原子谓词公式P(x) 表示 x 是有理数 Q(x) 表示 x 是实数（x

10、）P(x) => Q(x)（彐x）Q(x) P(x) (（x）Q(x) => P(x) 等价于 （彐x）Q(x) P(x)例： 每一个人的外祖父都是他母亲的父亲。令 P(x) 表示 x 是人O(x,y) 表示 x 是y的外祖父F(x,y) 表示 x 是y的父亲M(x,y) 表示 x 是y的母亲将原句转化为：每一个人y的外祖父x都是该y的母亲z的父亲。（x）（y）(P(x)P(y)O(x,y)=>(彐z)(P(z)F(x,z)M(z,y) 第二节 谓词公式5.2.1 谓词公式的定义原子谓词公式 P(x1，x2，xn）合适公式：1.原子谓词公式是合适公式。2.若A为合适公式，则A

11、也是一个合适公式。 5.若A和B都是合适公式，则（AB），（AB），（AB）和（A B）也都是合适公式。.若A是合适公式，x为任意变元，则（x）A和（彐x）A都是合适公式。.只有按上述规则1至4求得的那些公式，才是合适公式。5.2.2 合适公式的性质 如果P和Q是两个合适公式，则由这两个合适公式所组成的复合表达式可由下列真值表给出。 P Q PQ PQ P =>Q P T T T T T F F T T F T T T F T F F F F F F F T T 如果两个合适公式，无论如何解释（取任何值），其真值表都是相同的，那么我们就称此两合适公式是等价的。 有如下等价关系：1. 否定

12、之否定（P） 等价于 P2. PQ 等价于 PQ5. 狄·摩根定律（PQ） 等价于 PQ（PQ） 等价于 PQ5.分配律P（QR） 等价于 （PQ）（PR）P（QR）等价于（PQ）（PR）5.交换律PQ 等价于 QPPQ 等价于 QP6.结合律（PQ）R 等价于 P（QR）（PQ）R 等价于 P（QR）7.逆否律PQ 等价于 QP此外，我们还可建立下列等价关系：8. （彐x）P(x) 等价于 （x）(P（x）)（x）P(x) 等价于 (彐x)(P（x）)9. （x）P（x）Q（x） 等价于（x）P（x）（x）Q（x）（彐x）P（x）Q（x）等价于（彐x）P（x）（彐x）Q（x）10.

13、 （x）P（x） 等价于 （y）P（y）（彐x）P（x） 等价于 （彐y）P（y）上述最后两个等价关系说明，在一个量化的表达式中的约束变量是一个虚元，它可以用任何一个不在表达式中出现过的其他变量符号来代替。 下面用谓词演算来表示英文句子：All blocks on top of blocks that have been moved or that are attached to block that have been moved also have been moved. 可表示为：（x）（y）BLOCK（x）BLOCK（y）ONTOP（x，y）ATTACHED（x，y）MOVED（y）M

14、OVED（x）5.2.3 推理规则、定理与证明假元推理 合适公式结论W2 W1W1W2 前提全称消去推理（全称化推理）它是由合适公式（x）W(x)产生合适公式W(A)，其中A为任意常量符号。同时应用假元推理和全称化推理，可由合适公式(x)W1(x)W2(x)结论W2(A)W1（A） 推理规则用来由已知的合适公式产生导出的合适公式。在谓词逻辑中，这种导出的合适公式叫做定理，而所使用的推理规则的序列则构成该定理的一个证明。在人工智能中，可以把某些问题求解任务当做某个定理求证的任务。在该证明中所应用的推理序列给出了该问题的一个解答。5.2.4 永真性和可满足性永真： 一个公式如果它们对所有可能的解释

15、均取值T，则这个公式称作为永真的，而永真的基公式一般叫做重言式。如：公式P（A）P（A）P（B）公式G的一个解释I： 由非空域D以及对G中的常量符号、函数符号、谓词符号的一组指定所构成。公式G称为可满足的： 如果存在解释I，使G在I下取T值。公式G称为永真的： 如果G的所有解释I，都使G取T值。如果每个满足公式集S的解释也满足公式X，那么公式X逻辑上遵循公式集S。 凡使S中各公式为真者，必使公式X为真 X是S的逻辑结论例如： 结 论 X 前 提 S 公式 逻辑上遵循的公式集P（A） （x）P（x）（x）Q（x） （x）P（x）Q（x），（x）P（x）5.2.4 置换与合一 上一节讲过，联合使用

16、假元推理和全称化推理，可以根据合适公式 （x）W1（x）W2（x） W1（A）产生 W2（A）这就需要寻找A对x的置换，使W1（A）与W1（x）一致。寻找项对变量的置换，以使表达式一致，叫做合一。合一是人工智能中很重要的过程。置换 ： 在一个表达式（谓词公式）中用项（常量、变量、函数）去替换变量目的 ： 使多个表达式一致起来（以便进行归结推理）例： 表达式Px，f（y），B的四个置换为： s1=z/x，w/y s2=A/y s3=g（z）/x，A/y s4=c/x，A/y 一般形式为： t1/V1,t2/V2, ,tn/Vn其中ti 为项，Vi 为互不相同变量，且Vi不出现于ti中，表示Vi同

17、时替换为ti 设表达式E经置换S作用后，结果表达式为ES。则： Px，f（y），Bs1 = Pz，f（w），B Px，f（y），Bs2 = Px，f（A），B Px，f（y），Bs3 = Pg（z），f（A），B Px，f（y），Bs4 = Pc，f（A），B置换后的结果表达式ES为原表达式E的逻辑结论即ES在逻辑上遵循EES 也称为E在 代换S下的一个例式 越置换，越具有特殊性 P(x) A/x P(A) 一般 特殊置换满足结合律，但一般不满足交换律。即用s1s2表示两个置换s1与s2的合成，L表示一表达式，则有：（Ls1）s2 = L（s1s2）即用s1、s2相继作用于L是同 s1s2作用

18、于L一致的以及 （s1s2）s3=s1（s2s3）但 s1s2s2s1定义： 设有表达式集Ei = E1 ，E2 ，En，若存在置换S，使E1S = E2 S = = EnS ，则称S为集Ei的一个合一者（简称合一），也说表达式集是可合一的。例： P(a，y)，P(x，f(b)是可合一的 （因为存在置换 S =a/x,f(b)/y 是这个集的一个合一者）又例：Px，f（y），B，Px，f（B），B是可合一的，合一者为： S=A/x，B/y （实际上 A/x 多余的）另一合一者 g =B/y定义： 若g为Ei的一个合一者，对Ei的任一合一者S，都存在一个置换S，使得 EiS=Ei g S，则称g

19、为Ei的最通用（最简单的）合一者，记为mgu（Most General Unifier）。 如对上例，mgu为： g=B/y有许多算法可用来合一可合一表达式的有限集，并在该集不可合一时宣告失败退出。求mgu的算法：非递归算法 定义： 设有一非空有限公式集F= F1 ，F2 ，Fn，从F中各公式的第一个符号同时向右比较，直到发现第一个彼此不尽相同的符号止；从F的各个公式中取出那些从第一个不一致符号开始的最大子表达式，将这些子表达式作为元素组成一个集合D，称为F的分歧集。如 F=Px，f(y，z)，Px，f(g(a),h(b) F的分歧集 D = y,g(a)合一算法：1、置 k=0; Fk =

20、F;k =; (其中Fk 为消除了k个分歧集后的公式集；F为原始公式集；k 为消除了前k个分歧集所用的置换； 空置换）2、若Fk 只含一个表达式，则算法停止，k 为所求最一般合一；3、找出Fk 分歧集Dk ；4、若Dk 中存在元素ak 和tk ,其中ak 为变量，tk为项，且ak 不在tk中出现，则置k+1=k· tk /ak ；Fk+1=Fk· tk /ak ； k = k +1; 转步骤2；5、（第四步不满足，算法停止，F的最一般合一者不存在）例：求公式集Pa，x，f(g(y)，Pz，h(z,u)，f(u)的最一般合一者 mgu。解： k=0; F0 = F; 0 =;

21、 F0 不是单一元素集，有 D0 =a ,z1=0· a /z =· a /z = a /z ；F1=F0· a /z =Pa，x，f(g(y)，Pa，h(a,u)，f(u)；k=1; F1 不是单一元素集，有 D1 =x ,h(a,u)2=1· h(a,u) /x = a /z · h(a,u) /x = a /z, h(a,u) /x ；F2=F1· h(a,u) /x =Pa，h(a,u)，f(g(y)，Pa，h(a,u)，f(u)； k=2; F2 非单一，有 D2 =g(y) ,u3=2· g(y) /u = a

22、/z, h(a,g(y) /x, g(y) /u ；F3=F2· g(y) /u =Pa，h(a, g(y)，f(g(y)； k=3;F3 已为单一元素集 3= a /z, h(a,g(y) /x, g(y) /u 为公式集F的mgu(2) 递归算法（类PASCAL描述的UNIFY递归过程）Procedure unify(E1，E2) E1，E2为本层次带来欲合一的表达式 字符串型局部变量：F1 ,F2 ,T1 ,T2 ,Z1 ,Z2 , G1 ,G2 ; F1 ,F2 中存本次E1，E2的First元素 T1 ,T2 中存本次E1，E2的Tail部分 Z1 中存F1 ,F2 的合一

23、者，Z2中存T1 ,T2的合一者 首元素F1 ,F2 的合一者Z1 作用于剩余部分T1 ,T2后的结果放G1 ,G2 BEGINif E1或E2中有一个是原子（即谓词符号、函数符号、常量符号、否定符号或变量）then 递归出口 beginif E1和E2是相同的，thenreturn NIL;不用置换，就已相同 if E1非原子 then 交换E1和E2的位置,使E1是原子; if E1是变量,且E1不出现在E2中 then returnE2/E1 ; if E2是变量then returnE1/E2 else return FAIL; end else E1,E2均非原子时begin F1:

24、=E1的第一个元素;T1:=E1的其余元素;F2:=E2的第一个元素;T2:=E2的其余元素; Z1:=unify(F1,F2);将首元素合一，合一式在Z1中 if Z1=FAIL then return FAIL; 首元素不可合一， 则整体不可合一 G1：=Z1作用到T1的结果； G2：=Z1作用到T2的结果； Z2：=unify(G1，G2）；将剩余部分当作新表达式去合一，递归调用 if Z2=FAIL then return FAIL；return Z1与Z2的合成Z1·Z2endEND.递归具体实现方案将各种单括号及逗号视为元素及原子加入递归之中原子：（1）谓词符号、常量符号

25、、变量符号、函数符号、否定符号 (2)各种单括号： 圆、方、花括弧(3)逗号E1、E2的第一个元素为：谓词符号、常量符号、变量符号、函数符号(参数部分)、否定符号、单括号、逗号若F1与F2均为函数时，则令F1、F2均取函数符号部分，而将括号中的参数部分划归至T1、T2，再去递归处理。（否则的话，连同参数部分一起拿出当作第一元素）例：E1=Pa，x，f(g(y)E2=Pz，h(z,u)，f(u)则： unify(E1,E2); Z1:=unify(P,P)Z2:= unify(a ,.,z,) return Z1·Z2取值分析第i层次 F1值 F2值 Z1值 F1属性 F2属性 1 P

26、 P 谓词符号 谓词符号 2 方括号 方括号 3 a z a/z 常量符号 变量符号 4 ， ， 5 x h(a,u) h(a,u)/x 变量 函数符号(参数) 6 , , 逗号 逗号 7 f f 函数符号 函数符号 8 ( ( 圆括号 圆括号 9 g(y) u g(y)/u 函数符号(参数) 变量 10 ) ) 圆括号 圆括号 11 方括号 方括号 第三节 归结原理定义 归结: 是一种可用于一定的子句公式的重要推理规则。子句: 定义为由文字的析取组成的公式文字: 一个原子公式和原子公式的否定结论： 任意谓词公式都可化为子句集5.5.1 将谓词公式化为子句集的步骤1. 消去蕴涵符号 =>

27、只应用和符号， AB 替换 AB2. 的深入 （反复应用狄·摩根定律）AB 代替 （AB）AB 代替 （AB）A 代替 （A）（x）A 代替 （彐x）A（彐x）A 代替 （x）A5. 量词变元唯一（变量标准化）在任一量词辖域内，受该量词约束的变量为一哑元（虚构变量），它可以在该辖域内处处统一地被另一个没有出现过的任意变量所代替，而不改变公式的真值。合适公式中变量的标准化意味着对哑元改名以保证每个量词有其自己唯一的哑元。例如，（x）P（x）（彐x）Q（x）标准化而得到： （x）P（x）（彐y）Q（y）4. 消去 彐存在量词是在全称量词的辖域内，我们允许所存在的x可能依赖于y值。令这种依

28、赖关系明显地由函数g（y）所定义，它把每个y值映射到存在的那个x。这种函数叫做Skolem函数。如果用Skolem函数代替存在的x，我们就可以消去全部存在量词,但函数符号不能同于公式中已有函数。 如： （x）（y）（彐z） P（x，y,z） 消去 彐, 写成 （x）（y）P（x，y,f(x,y)） ii) 如果要消去的存在量词不在任何一个全称量词的辖域内，那么我们就用不含变量的Skolem函数即常量代换。 例如，（彐x）P（x）化为P（A） 其中常量符号A用来表示我们知道的存在实体。A必须是个新常量符号，它未曾在公式中其他地方使用过。5. 化为前束形到这一步，已不留下任何存在量词，而且每个全称

29、量词都有自己的变量。把所有全称量词移到公式的左边，并使每个量词的辖域包含这个量词后面公式的整个部分。所得公式称为前束形。前束形公式由前缀和母式组成，前缀由全称量词串组成，母式由没有量词的公式组成，即： 前束形 =（前缀） 母 式 全称量词串 无量词公式6. 把母式化为合取范式 任何母式都可写为由一些谓词公式和（或）谓词公式的否定的析取的有限集组成的合取。这种母式叫做合取范式。我们可以反复应用分配律，把任一母式化成合取范式。例如， 把ABC化为： ABAC7. 消去全称量词 到了这一步，所有余下的量词均被全称量词量化了。同时，全称量词的次序也不重要了。因此，我们可以消去前缀，即消去明显出现的全称

30、量词。8. 消去连词符号用A，B代替（AB），以消去明显的符号。反复代替的结果，最后得到一个有限集，其中每个公式是文字的析取。9. 更换变量名称 可以更换变量符号的名称，使一个变量符号不出现在一个以上的子句中。例 将下列谓词公式 （x）P（x）（y）P(y)P(f(x,y)（y）Q(x,y)P（y）按标准步骤化为子句集。解： (1) (x)P(x)(y)P(y)P(f(x,y) (y)Q（x，y）P（y）(2) (x)P（x）(y)P(y)P(f(x,y) （彐y）Q（x，y）P（y）(x)P（x）(y)P(y)P(f(x,y) （彐y）Q（x，y）P（y）(3) (x)P（x）(y)P(y)

31、P(f(x,y)（彐w）Q（x，w）P（w）(4) (x) P（x）(y)P(y)P(f(x,y)Q（x，g（x）P（g（x） 式中，g（x）为一Skolem函数。(5) (x)(y)P（x）P(y)P(f(x,y)Q（x，g（x）P（g（x）(6) (x)(y)P（x）P（y）P（f（x，y）P（x）Q（x，g（x）P（x）P（g（x）(7) P（x）P（y）P（f（x，y）P（x）Q（x，g（x）P（x）P（g（x）(8) P（x）P（y）P（f（x，y） P（x）Q（x，g（x） P（x）P（g（x）(9)更改变量名称，在上述第(8)步的三个子句中，我们分别以x1，x2和x3代替变量x。

32、这种更改变量名称的过程，有时称为变量分离标准化。于是，我们可以得到下列子句集：P（x1）P（y）Pf（x1，y）P（x2）Qx2，g（x2）P（x3）Pg（x3）必须指出，一个子句内的文字可含有变量，但这些变量总是被理解为全称量词量化了的变量。如果一个表达式中的变量被不含变量的项所置换，则我们得到称为文字基例的结果。例如，QA，f（g（B）就是Q（x，y）的一个基例。在定理证明系统中，归结作为推理规则使用时，我们希望从公式集来证明某个定理，首先就要把公式集化为子句集。可以证明，如果公式X在逻辑上遵循公式集S，那么X在逻辑上也遵循由S的公式变换成的子句集。即当希望证明: “若公式集S成立,则可推

33、出X成立。”可变为证明：若公式集S变换成的子句集成立,则可推出X成立。5.5.2 归结推理规则令L1为任一原子公式，L2为另一原子公式；L1和L2具有相同的谓词符号，但一般具有不同的变量；L2为L2的否定。结论： 若两子句具有形式L1和L2，且L1和L2具有最一般合一者时，则任一使L1及L2为真的解释必使()·为真。即是说()·必为两前提子句L1及L2的逻辑结论 ；或说可从两父辈子句推导出新子句，叫归结式。它是由取这两个子句的析取，然后消去互补对而得到的。推论： 两前提子句具有形式L112i及L112j则可导出结论子句 12i12j例： 前提1 前提2 结论（归结式）PR

34、PQ RQPQR QS PRSP PQ QPQ PQ QQ = QPQ PQ QQ Q=>Q 重言式PP P=>PP P ？PQ QR PR 链环式(三段论)5.5.3 含有变量子句的归结让我们把上述简单的对基子句的归结推理规则推广到含有变量的子句。情况1： （有明显互补）P(X) Q(X) P（X）R(f(A) 归结式 Q(X)R(f(A)情况2： （靠合一产生互补）P(x,f(y) Q(x) R(f(a),y)R(z,w) P（f(f(a),z）令 = f(f(a)/x, f(y)/z 有归结式：Q(f(f(a) R(f(a),y) R(f(y),w) 归结两个子句时，可能有一

35、个以上的归结式，但任何情况下，最多只有有限个归结式。 一般归结规则：设有两个子句 Li与Mi，若 li 是Li的一个子集，mi是Mi的一个子集，且存在一个最一般合一者s, 使得 lis=mis ,则可归结前提子句Li与Mi成为Li-lisMi-mis例：我们考虑两个子句：Px，f（A）Px，f（y）Q（y）和 Pz，f（A）Q（z） 如果我们取 li = Px，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）可

36、见对这两个子句归结一共可得四个不同的归结式，其中三个是归结P得到的，而另一个是由归结Q得到的。第四节 谓词演算在定理证明中的应用 在典型的定理证明系统中，归结通过反演产生证明。也就是说，要证明某个命题，其目标公式被否定并化成子句形，然后添加到命题公式集中去，把归结反演系统应用于联合集，并推导出一个空子句（NIL），表示产生一个矛盾，从而使定理得到证明。这种归结反演的证明思想，与数学中反证法的思想十分相似。 5.4.1 归结反演设有前提公式集S，欲证结论公式L。步骤如下： (1)否定L，得L； (2)把L添加到S中去； (3)把新产生的集合L，S化成子句集； (4)应用归结原理，力图推导出一个表

37、示矛盾的空子句。归结反演的正确性。公式L在逻辑上遵循公式集S 任一使S为真的解释必使L为真，即是说：不存在这样的解释，它使S与L同时为真，也即SL是不可满足的。 SL是不可满足的能从S，L子句集通过多次归结操作产生一个空子句NIL例：前提： 每个储蓄钱的人都获得利息。 结论： 如果没有利息，那么就没有人去储蓄钱。 证明： 令S（x，y）表示“x储蓄y”M（x）表示“x是钱”I（x）表示“x是利息”E（x，y）表示“x获得y”于是我们可把上述命题写成下列形式：前提： ( x)（彐y）(S(x,y)M(y)（彐y）(I(y)E(x,y)结论：（彐x）I(x)(x) (y)(S(x,y)M(y) 把

38、前提化为子句形： ( x) （彐y）(S(x,y)M(y)（彐y）(I(y)E(x,y) ( x)( y) (S(x,y) M(y)（彐y）(I(y)E(x,y) 令y=f(x)为Skolem函数,则可得子句形如下： (1)S（x，y）M（y）I(f(x) (2)S（x，y）M（y）E(x，f(x) 又结论的否定为： (彐x)I(x)(x)( y)(S(x,y)M(y) 化为子句形： (彐x)I(x)(x)( y)(S(x,y)M(y) (彐x)I(x)(x)( y)(S(x,y)M(y)(x)(I(x)(彐x)(彐y)(S(x,y)M(y)变量分离标准化之后得下列各子句：(3)I（z） (4

39、)S（a，b） (5)M（b）子句(1) 子句(3) f(x)/zS(x,y)M(y)子句(6) 子句(4) a/x,b/yNILM(b) 子句(7) 子句(5) 储蓄问题反演树例: 对于所有的x和y，如果x是y的父亲，y是z的父亲，那么x是z的祖父。每个人都有一个父亲。是否会有这样的两个人x和y，使得x是y的祖父？证明： 令 F(x,y)表示“x是y的父亲” G(x,y)表示“x是y的祖父”把命题写成下列公式： (1) (x) (y) (z) (F(x,y)F(y,z)G(x,z) (2) (y)(彐x) F(x,y) (3) (彐x)(彐y)G(x,y)其中，公式(3)是我们试图证明的结论

40、。 将公式(1)、(2)化为子句形，得：（1）F（x，y）F（y，z）G（x，z）（2）F（f（w），w）x=f（w）为一Skolem函数取公式(3)的否定： (3) (彐x)(彐y)G(x,y) 得其子句形为： （3）G（u，v）子句(1) 子句(3) u/x,v/zF(u ,y)F(y ,v) 子句(2) f(w)/y,v/wF(u , f(v) 子句(2) f(w)/u,f(v)/w NIL 祖孙问题反演树 归结反演系统的基本算法： 设已把各前提式与结论式的否定化成了所要求的子句集形式,并放在集合S中(1) CLAUSES S(2) WHILE NIL不为CLAUSES 的成员 do(3

41、) begin(4) 在CLAUSES中选取两个不同的可归结子句ci和cj(5) 计算ci和cj的归结式rij(6) 把rij附加到子句集中，产生新的子句集(7) end如: (1)PQ (2) PQ (3)PQ (4) PQ可归结的子句对有:直接应用归结原理，将对应于一个反演的简单的宽度优先搜索。宽度优先搜索方法:第i级归结式是这样的归结式,其最近的父辈子句之一是第i-1级的归结式,而另一父辈子句则为第0至第i-1级之中的任一子句。具体做法是： 首先将S0（第0级即初始子句集）的子句排序。之后，顺序考虑S0 与S0之间的归结式，得第一级归结式集合S1=C12|C1S0，C2S0，然后检查NI

42、L是否S1，是则结束，否则继续考虑S0S1与S1之间的归结式，得第二级归结式集合S2=C12|C1S0S1，C2S1，然后检查NIL是否S2，如： (1) PQS0: (2) PQ (3) PQ (4) PQ (5) Q 1-2 (6) P 1-3 (7) QQ 1-4(i) S1: (8) PP 1-4(ii) (9) QQ 2-3(i) (10) PP 2-3(ii) (11) P 2-4 (12) Q 3-4 S2: ? NIL ?例： 前提 （1）(x) R(x)=>L(x) 任何能阅读的人都是能识字的。（2）(x) D(x)=> L(x) 任何海豚都不识字。（3）(彐x)

43、 D(x) I(x) 有些海豚是有智力的。 结论：（4）(彐x) I(x) R(x) 有些有智力者不能阅读。 解： 将(1)(2)(3)及(4)的否定化成子句集： (1) I(A)S0: (2) I(z)R(z) (3) R(x) L(x)(4) D(y)L(y) (5) D(A) (6)R(A) 1-2 A/zS1: (7) I(z)L(z) 2-3 z/x(8) R(y) D(y) 3-4 y/x (9) L(A) 4-5 A/y (10) L(A) 1-7 A/z (11) I(z) D(z) 2-8 z/y (12) L(A) 3-6 A/x S2: (13) R(A) 3-9 A/x

44、 (14) I(z) D(z) 4-7 z/y (15) R(A) 5-8 A/y (16) D(A) 6-8 A/y (17) I(A) 7-9 A/z S3 ? NIL ?归结搜索策略基本上可分为三种类型：简化策略、改进策略和排序策略。5.4.2 简化策略若某子句集是不可满足的经过若干次下述三种消去后的该子句集是不可满足的1.重言式消去法 若某子句中含有一个文字及其否定的话，则可消去该子句。例如，子句 P（x）B（y）B（y）和 P（f（A）P（f（A）均可消去。2.谓词估算消去法若某子句中某一文字估算为T，则可消去该文字所在的那一个子句。 若某子句中某一文字估算为F，则可消去该文字。例如，设E(x,y)表示x=y，那么子句P（x）Q（