第5章基于一阶谓词的机器推理 基于一阶谓词（firstorder predicate）的机器推理也称自动推理，它是早期人工智能的主要研究内容之一。一阶谓词是一种表达力很强的形式语言，而且这种语言很适合数字计算机处理,因而成为知识表示的首选。基于这种语言，不仅可以实现类似于人类推理的自然演绎法机器推理，而且也可实现不同于人类的归结(或称消解)法机器推理。本章主要介绍作为一种知识表示形式的一阶谓词和基于它的机器推理。 5.1一阶谓词逻辑 5.1.1谓词，函数，量词 定义51表达式 P(t1，t2，…，tn) 称为一个n元谓词，或简称谓词。其中，P是谓词名或谓词符号，也称谓词，表示对象的属性、状态、关系、联系或行为； t1，t2，…，tn被称为谓词的项，一般代表对象。 例如： prime(2) friend(张三,李四) 就是两个谓词。其中，prime(2)是一元谓词，表示“2是个素数”； friend(张三，李四)是二元谓词，表示“张三和李四是朋友”。 谓词中的项t1，t2，…，tn可以是代表具体事物的符号或数值，这样的项被称为个体常元； 也可以是取不同的值的变元，这样的项被称为个体变元。显然，当项t1，t2，…，tn全为常元时，P(t1，t2，…，tn)就表示一个命题。但当项t1，t2，…，tn中含有变元时，P(t1，t2，…，tn)则是一个命题形式，称为(n元)命题函数或谓词命名式。个体变元的取值范围被称为个体域(或论述域)，包揽一切事物的集合则称为全总个体域。 由于谓词有严格的语法格式，所以，谓词实际上就是一种形式语言。它可以表示自然语言命题。换句话说，谓词就是自然语言命题的一种形式化表示。 同一个个体域的个体之间往往存在某种对应关系。例如在人类集合中，每一个人都有一个母亲。又如在实数域中任何两个数都有它们的和与之对应。为了表达个体之间的对应关系，谓词逻辑中通常借用数学中函数的概念和记法，用如下形式 f(x1，x2，…，xn) 表示个体x1，x2，…，xn所对应的个体y，并称之为(n元)个体函数，简称函数(或函词、函词命名式)，其中f是函数符号。有了函数的概念和记法，谓词的表达能力就更强了。例如，可用doctor(father(Li))表示“小李的父亲是医生”，用equa(sq(x)，y)表示“x的平方等于y”。 下面约定用大写英文字母作为谓词符号，用小写字母f、g、h等表示函数符号，用小写字母x、y、z等作为个体变元符号，用小写字母a、b、c等作为个体常元符号。 在谓词逻辑中，将“所有”“一切”“任一”“全体”“凡是”等词统称为全称量词（universal quantifier），记为； “存在”“一些”“有些”“至少有一个”等词统称为存在量词(existential quantifier)，记为。 引入量词后，谓词的表达能力被进一步扩充。例如命题“凡是人都有名字”，就可以表示为 x(P(x)→N(x)) 其中,P(x)表示“x是人”，N(x)表示“x有名字”，该式可读作“对于任一x，如果x是人，则x有名字”。这里的个体域取为全总个体域。如果把个体域取为人类集合，则该命题就可以表示为: xN(x) 同理，可以把命题“存在不是偶数的整数”表示为: x(I(x)∧瘙綈E(x)) 其中I(x)表示“x是整数”，E(x)表示“x是偶数”。此式可读作“存在x，x是整数并且x不是偶数”。 紧接于量词之后被量词作用(即说明或限定)的命题函数式被称为该量词的辖域。例如： (1) xP(x) (2) x(H(x)→G(x，y)) (3) xA(x)∧B(x) 其中，(1)中的P(x)为全称量词的辖域，(2)中的H(x)→G(x，y)为全称量词的辖域，(3)中的A(x)为存在量词的辖域，但B(x)并非的辖域。 量词后的变元被称为量词的指导变元(或作用变元)，而在一个量词的辖域中与该量词的指导变元相同的变元被称为约束变元，其他变元(如果有的话)则被称为自由变元。 例如x、y中的x、y分别是量词、的指导变元； 上面(2)式中的x为约束变元，而y则为自由变元，(3)式中A(x)中的x为约束变元，但B(x)中的x为自由变元。一个变元在一个公式中既可约束出现，又可自由出现，但为了避免混淆，往往通过改名，使得一个公式中的变元仅以一种形式出现。例如上面的(3)式通过改名就变为 (3′) xA(x)∧B(y) 约束变元的改名规则如下： (1) 对需改名的变元，应同时更改该变元在量词及其辖域中的所有出现。 (2) 新变元符号必须是量词辖域内原先没有的，最好是公式中也未出现过的。 例如公式xP(x)∧Q(x)可改为yP(y)∧Q(x)，但二者的意义相同。 在谓词前加上量词，称作谓词中相应的个体变元被量化，例如xA(x)中的x被量化，yB(y)中的y被量化。如果一个谓词中的所有个体变元都被量化，则这个谓词就变为一个命题了。例如，设P(x)表示“x是素数”，则xP(x)和xP(x)都是命题。这样就有两种从谓词(即命题函数)得到命题的方法： 一种是给谓词中的个体变元代入个体常元，另一种就是把谓词中的个体变元全部量化。 需要说明的是，仅个体变元被量化的谓词称为一阶谓词。如果不仅个体变元被量化，而且函数符号和谓词符号也被量化，那样的谓词则称为二阶谓词。本书只涉及一阶谓词，所以，以后提及的谓词都是指一阶谓词。 如果一个命题形式中的所有个体变元都被量化，或者所有变元都是约束变元(或无自由变元)，则这个命题形式就是一个命题。特别地，称xA(x)为全称命题，xA(x)为特称命题。对于这两种命题，当个体域为有限集时(设有n个元素)，有下面的等价式 xA(x)A(a1)∧A(a2)∧…∧A(an) xA(x)A(a1)∨A(a2)∨…∨A(an) 这两个式子也可以推广到个体域为可数无限集。 5.1.2谓词公式 定义52 (1) 个体常元和个体变元都是项。 (2) 设f是n元函数符号，若t1，t2，…，tn是项，则f(t1，t2，…，tn)也是项。 (3) 只有有限次使用(1)(2)得到的符号串才是项。 定义53设P为n元谓词符号，t1，t2，…，tn是项，则P(t1，t2，…，tn)称为原子谓词公式，简称原子公式或者原子。 从原子谓词公式出发，通过命题联结词和量词，可以组成复合谓词公式。下面给出谓词公式的严格定义，即谓词公式的生成规则。 定义54 (1) 原子公式是谓词公式。 (2) 若P，Q是谓词公式，则瘙綈P，P∧Q，P∨Q，P→Q，P←→Q，xP，xP也是谓词公式。 (3) 只有有限步应用(1)、(2)生成的公式才是谓词公式。 由项的定义，当t1，t2，…，tn全为个体常元时，所得的原子谓词公式就是原子命题公式。所以，全体命题公式也都是谓词公式。谓词公式也称为谓词逻辑中的合适(式)公式，记为Wff。 定义55设G为如下形式的谓词公式： P1∧P2∧…∧Pn 其中，Pi(i=1，2，…，n)形如L1∨L2∨…∨Lm，Lj(j=1，2，…，m)为原子公式或其否定，则G称为合取范式。 例如： (P(x)∨Q(y))∧(P(x)∨瘙綈Q(y)∨R(x，y))∧(瘙綈Q(y)∨R(x，y)) 就是一个合取范式。 应用逻辑等价式，任一谓词公式都可以化为与之等价的合取范式，这个合取范式就称为原公式的合取范式。一个谓词公式的合取范式一般不唯一。 定义56设G为如下形式的命题公式： P1∨P2∨…∨Pn 其中，Pi(i=1，2，…，n)形如L1∧L2∧…∧Lm，Lj(j=1，2，…，m)为原子公式或其否定，则G称为析取范式。 例如： (P(x)∧Q(y)∧R(x，y))∨(P(x)∧瘙綈Q(y))∨(瘙綈P(x)∧瘙綈R(x，y)) 就是一个析取范式。 应用逻辑等价式，任一谓词公式都可以化为与之等价的析取范式，这个析取范式被称为原公式的析取范式。同样，一个谓词公式的析取范式一般也不唯一。 定义57谓词公式G在个体域D中的一个解释I是指： (1) 对G中每一个常元符号指定D中的一个元素。 (2) 对G中每一个n元函数符号指定一个函数，即Dn到D的一个映射。 (3) 对每个n元谓词符号指定一个谓词，即Dn到{T，F}的一个映射。 例51设谓词公式G=x(P(f(x))∧Q(x，f(a)))，给出如下的一个解释I： D={1,2} a1 f(1)2,f(2)1 P(1)F，P(1)T,Q(1，1)T,Q(1，2)T,Q(2，1)F,Q(2，2)T 因为x=1时， P(f(x))∧Q(x，f(a))=P(f(1))∧Q(1，f(1))=P(2)∧Q(1，2)=T∧T=T 所以，谓词公式G在I下为真。 定义58设G、H是两个谓词公式，D是它们的公共个体域，若对于D中的任一解释，G、H有相同的真值，则称公式G、H在个体域D上逻辑等价。若G、H在所有个体域上等价，则称G、H逻辑等价，记为GH。 定义59设G、H是两个谓词公式，D是它们的公共个体域，若对于D中的任一解释，当G真时H也真，则称在个体域D上公式G逻辑蕴涵公式H。若在所有个体域上G都逻辑蕴涵H，则称G逻辑蕴涵H，或称H是G的逻辑结果，记为GH。 由上面的两个定义，可以证明下面的定理。 定理51设G、H是两个谓词公式，GH的充分必要条件是GH且HG。 表51和表52所列的就是形式逻辑中常用的一些逻辑等价式和逻辑蕴涵式。 表51常用逻辑等价式 E1瘙綈瘙綈PP双重否定律 E2P∧PP E3P∨PP等幂律 E4P∧QQ∧P E5P∨QQ∨P交换律 E6(P∧Q)∧RP∧(Q∧R) E7(P∨Q)∨RP∨(Q∨R)结合律 E8P∧(Q∨R)(P∧Q)∨(P∧R) E9P∨(Q∧R)(P∨Q)∧(P∨R)分配律 E10P∧(P∨Q)P E11P∨(P∧Q)P吸收律 E12瘙綈(P∧Q)瘙綈P∨瘙綈Q E13瘙綈(P∨Q)瘙綈P∧瘙綈Q摩根律 E14P→Q瘙綈P∨Q蕴含表达式 E15P←→Q(P→Q)∧(Q→P) E16P∧TP E17P∧FF E18P∨TT E19P∨FP等价表达式 E20P∧瘙綈PF矛盾律 E21P∨瘙綈PT排中律 E22P→(Q→R)P∧Q→R输出律 E23(P→Q)∧(P→瘙綈Q)瘙綈P归谬律 E24P→Q瘙綈Q→瘙綈P逆否律 E25xPPP中不含约束变元x E26xPPP中不含约束变元x E27x(A(x)∧B(x))xA(x)∧xB(x) E28x(A(x)∨B(x))xA(x)∨xB(x)量词分配律 E29瘙綈xA(x)x瘙綈A(x) E30瘙綈xA(x)x瘙綈A(x)量词转换律 E31xA(x)∧Px(A(x)∧P) E32xA(x)∨Px(A(x)∨P) E33xA(x)∧Px(A(x)∧P)量词辖域扩张及收缩律 E34xA(x)∨Px(A(x)∨P) E35xyP(x，y)yxP(x，y)(P为不含约束变元x的谓词公式) 续表 E36xyP(x，y)yxP(x，y) E37xA(x)→Px(A(x)→P) E38xA(x)→Px(A(x)→P) E39P→xA(x)x(P→A(x)) E40P→xA(x)x(P→A(x))(P为不含约束变元x的谓词公式) 表52常用逻辑蕴涵式 I1PP∨Q附加律 I2P∧QP，P∧QQ简化律 I3(P→Q)∧PQ假言推理(分离规则) I4(P→Q)∧瘙綈Q瘙綈P拒取式 I5(P∨Q)∧瘙綈PQ析取三段论 I6(P→Q)∧(Q→R)P→R假言三段论 I7P→Q(Q→R)→(P→R) I8(P→Q)∧(R→S)P∧R→Q∧S I9(P←→Q)∧(Q←→R)P←→R I10P，QP∧Q合取式 I11xA(x)A(y)y是个体域中任一确定元素，全称指定规则(Universal Specification,US) I12xA(x)A(y)y是个体域中某一确定元素，存在指定规则(Existential Specification，ES) I13A(y)xA(x)y是个体域中任一确定元素，全称推广规则(Universal Generalization，UG) I14A(y)xA(x)y是个体域中某一确定元素，存在推广规则(Existential Generalization，EG) I15xA(x)xA(x) I16xA(x)∨xB(x)x(A(x)∨B(x)) I17x(A(x)∧B(x))xA(x)∧xB(x) I18xyP(x，y)yxP(x，y) I19yxP(x，y)xyP(x，y) I20xyP(x，y)yxP(x，y) 5.1.3永真式与推理规则 定义510设P为谓词公式，D为其个体域，对于D中的任一解释I： (1) 若P恒为真，则称P在D上永真(或有效)或是D上的永真式。 (2) 若P恒为假，则称P在D上永假(或不可满足)或是D上的永假式。 (3) 若至少有一个解释，可使P为真，则称P在D上可满足或是D上的可满足式。 定义511设P为谓词公式，对于任何个体域： (1) 若P都永真，则称P为永真式。 (2) 若P都永假，则称P为永假式。 (3) 若P都可满足，则称P为可满足式。 由于谓词公式的真值与个体域及解释有关，考虑到个体域的数目和个体域中元素数目无限的情形，所以要通过一个机械地执行的方法(即算法)，判断一个谓词公式的永真性一般是不可能的，所以称一阶谓词逻辑是不可判定的(但它是半可判定的)。 定理52设G、H是两个谓词公式，则： G←→H永真的充分必要条件是GH G→H永真的充分必要条件是GH 由篇幅所限，该定理的证明从略。 我们知道，推理是由一个或几个命题(称为前提)得到一个新命题(称为结论)的(思维)过程。可以看出，若把一个推理过程符号化，其形式就是一个蕴涵式。一个正确有效的推理首先要求其推理形式必须正确。那么，怎样判断一个推理的形式是否正确呢？下面的定理53给出了回答。 定理53一个推理形式正确，当且仅当其对应的蕴涵式永真。 由篇幅所限，该定理的证明从略。 正确的推理形式是推理中应该遵循的形式，所以，在逻辑学中，正确的推理形式被称为推理规则。这样，由定理52和定理53可得，上面表52中的逻辑蕴涵式都是推理规则，而表51中的一个逻辑等价式则可以分解为两个推理规则。 5.1.4自然语言命题的谓词形式表示 由上所述，利用谓词公式这种形式语言可以将自然语言中的陈述语句严格地表示为一种符号表达式。将自然语言命题用谓词形式表示的一般方法是： (1) 简单命题可以直接用原子公式来表示。 (2) 复合命题则需要先找出支命题，并将其符号化为原子公式，然后根据支命题之间的逻辑关系选用合适的连接词(瘙綈,∧,∨，→，←→)和量词(，)将这些原子公式连接起来。 一般来说，一个复合命题的形式化表示法并不唯一，即同一个复合命题可能符号化为不同形式的谓词公式。 由于不同的个体变元可能有不同的个体域，为了方便和统一起见，用谓词公式表示命题时，一般总取全总个体域，然后再采取使用限定谓词的办法来指出每个个体变元的个体域。具体来讲，就是： (1) 对全称量词，把限定谓词作为蕴涵式之前件加入，即x(P(x)→…)。 (2) 对存在量词，把限定量词作为一个合取项加入，即x(P(x)∧…)。 这里的P(x)就是限定谓词。 例52用谓词公式表示命题： 不存在最大的整数。 解用I(x)表示： x是整数，用D(x，y)表示： x大于y。则原命题就可形式化为： 瘙綈x(I(x))∧y(I(y)→D(x，y)) 或 x(I(x))→y(I(y)∧D(y，x)) 例53设有命题： 对于所有的自然数x、y，均有x+y>x。用谓词公式表示之。 解用N(x)表示： x是整数，S(x，y)表示函数： s=x+y，D(x，y)表示： x大于y，则原命题可形式化为谓词公式 xy(N(x)∧N(y)→D(S(x，y)，x)) 例54将命题“某些人对某些食物过敏”用谓词公式表示。 解用P(x)表示： x是人，用F(x)表示： x是食物，用A(x，y)表示： x对y过敏。则原命题可用谓词公式表示为 xy(P(x)∧F(y)∧A(x，y)) 需注意的是，全称量词与存在量词不满足交换律。从而， xyP(x，y)≠yxP(x，y) 事实上，如果将P(x，y)解释为： y是x的母亲，则xyP(x，y)的意思就是： 任何人都有母亲，而yxP(x，y)的意思则是： 有一个人她是所有人的母亲。 5.1.5基于谓词公式的形式演绎推理 上述从形式逻辑中抽象出来的推理规则也就是一些谓词公式的变换规则。这样，如果我们将待推理的前提命题表示成谓词公式，就可以利用推理规则把基于自然语言的逻辑推理转化为基于谓词公式的符号变换，即实现所说的形式推理。下面通过几个例子介绍基于谓词公式的形式演绎推理方法。 例55设有前提： (1) 凡是大学生都学过计算机； (2) 小王是大学生。 试问： 小王学过计算机吗？ 解令S(x)表示： x是大学生； M(x)表示： x学过计算机； a表示： 小王。则上面的两个命题可用谓词公式表示为 (1) x(S(x)→M(x)) (2) S(a) 下面遵循有关推理规则进行符号变换和推理： (1) x(S(x)→M(x))［前提］ (2) S(a)→M(a)［(1)，US］ (3) S(a)［前提］ (4) M(a)［(2)，(3)，I3］ 得结果： M(a)，即“小王学过计算机”。 例56证明： 瘙綈P(a，b)是xy(P(x，y)→W(x，y))和瘙綈W(a，b)的逻辑结果。 证 (1) xy(P(x，y)→W(x，y))［前提］ (2) y(P(a，y)→W(a，y))［(1)，US］ (3) P(a，b)→W(a，b)［(2)，US］ (4) 瘙綈W(a，b)［前提］ (5) 瘙綈P(a，b)［(3)，(4)，I4］ 例57证明： x(P(x)→Q(x))∧x(R(x)→瘙綈Q(x))x(R(x)→瘙綈P(x))。 证 (1) x(P(x)→Q(x))［前提］ (2) P(y)→Q(y)［(1)，US］ (3) 瘙綈Q(y)→瘙綈P(y)［(2)，E24］ (4) x(R(x)→瘙綈Q(x))［前提］ (5) R(y)→瘙綈Q(y)［(4)，US］ (6) R(y)→瘙綈P(y)［(3)，(5),I6］ (7) x(R(x)→瘙綈P(x))［(6)，UG］ 可以看出，上述的推理过程完全是一个符号变换过程。这种推理与人们用自然语言推理的思维过程十分相似，因而也被称为自然演绎推理。同时，这种推理实际上已几乎与谓词公式所表示的含义完全无关，而是一种纯形式的推理。这种形式推理是传统谓词逻辑中的基本推理方法。 由谓词公式的形式推理特点，人们自然想到将这种推理方法引入机器推理。但是，这种形式推理在机器中具体实施起来却存在许多困难。例如，推理规则太多、应用规则需要很强的模式识别能力、中间结论的指数递增等。所以，在机器推理中完全照搬谓词逻辑中的形式演绎推理方法，会有不少困难。于是，人们又开发了一些受限的自然演绎推理技术； 或者另辟蹊径，发明了所谓的归结演绎推理技术。 5.2归结演绎推理 5.2.1子句与子句集 定义512原子谓词公式及其否定称为文字，若干个文字的一个析取式称为一个子句，由r个文字组成的子句叫r文字子句，1文字子句叫单元子句，不含任何文字的子句称为空子句，记为□或NIL。 例如，下面的析取式都是子句： P∨Q∨瘙綈R P(x，y)∨瘙綈Q(x) 定义513对一个谓词公式G，通过以下步骤所得的子句集合S称为G的子句集。 (1) 消去蕴涵词→和等值词←→。 可使用逻辑等价式： ① P→Q瘙綈P∨Q ② P←→Q(瘙綈P∨Q)∧(瘙綈Q∨P) (2) 缩小否定词的作用范围，直到其仅作用于原子公式。 可使用逻辑等价式： ① 瘙綈(瘙綈P)P ② 瘙綈(P∧Q)瘙綈P∨瘙綈Q ③ 瘙綈(P∨Q)瘙綈P∧瘙綈Q ④ 瘙綈xP(x)x瘙綈P(x) ⑤ 瘙綈xP(x)x瘙綈P(x) (3) 适当改名，使量词间不含同名指导变元和约束变元。 (4) 消去存在量词。 消去存在量词时，同时还要进行变元替换。变元替换分两种情况： ① 若该存在量词在某些全称量词的辖域内，则用这些全称量词指导变元的一个函数代替该存在量词辖域中的相应约束变元，这样的函数被称为Skolem函数； ② 若该存在量词不在任何全称量词的辖域内，则用一个常量符号代替该存在量词辖域中的相应约束变元，这样的常量符号被称为Skolem常量。 (5) 消去所有全称量词。 (6) 化公式为合取范式。 可使用逻辑等价式： ① P∨(Q∧R)(P∨Q)∧(P∨R) ② (P∧Q)∨R(P∨R)∧(Q∨R) (7) 适当改名，使子句间无同名变元。 (8) 消去合取词∧，以子句为元素组成一个集合S。 例58求下面谓词公式的子句集。 x{yP(x，y)→瘙綈y［Q(x，y)→R(x，y)］} 解 由步骤(1)得x{瘙綈yP(x，y)∨瘙綈y［瘙綈Q(x，y)∨R(x，y)］} 由步骤(2)得x{y瘙綈P(x，y)∨y［Q(x，y)∧瘙綈R(x，y)］} 由步骤(3)得x{y瘙綈P(x,y)∨z［Q(x,z)∧瘙綈R(x,z)］} 由步骤(4)得x{瘙綈P(x，f(x))∨［Q(x，g(x))∧瘙綈R(x，g(x))］} 由步骤(5)得瘙綈P(x，f(x))∨［Q(x，g(x))∧瘙綈R(x，g(x))］ 由步骤(6)得［瘙綈P(x，f(x))∨Q(x，g(x))］∧［瘙綈P(x，f(x))∨瘙綈R(x，g(x))］ 由步骤(7)得［瘙綈P(x，f(x))∨Q(x，g(x))］∧［瘙綈P(y，f(y))∨瘙綈R(y，g(y))］ 由步骤(8)得{瘙綈P(x，f(x))∨Q(x，g(x)),瘙綈P(y，f(y))∨瘙綈R(y，g(y))} 或写为 瘙綈P(x，f(x))∨Q(x，g(x)) 瘙綈P(y，f(y))∨瘙綈R(y，g(y)) 这就是原谓词公式的子句集。 需说明的是，在上述求子句集的过程中，当消去存在量词后，把所有全称量词都依次移到整个式子的最左边(或者先把所有量词都依次移到整个式子的最左边，再消去存在量词)，再将右部的式子化为合取范式，这时所得的式子被 称为原公式的Skolem标准型。例如，上例中谓词公式的Skolem标准型就是: x{［瘙綈P(x，f(x))∨Q(x，g(x))］∧［瘙綈P(y，f(y))∨瘙綈R(y，g(y))］} 可以看出，消去Skolem标准型左部的全称量词和合取范式中的合取词，即得公式的子句集。 例59设G=xyzuvw(P(x，y，z)∧Q(u，v，w))，那么，用a代替x，用f(y，z)代替u，用g(y，z，v)代替w，则得G的Skolem标准型 yzv(P(a，y，z)∧瘙綈Q(f(y，z)，v，g(y，z，v))) 进而得G的子句集为 {P(a，x，y)，瘙綈Q(f(u，v),w，g(u，v，w))} 由此例还可看出，一个公式的子句集也可以通过先求前束范式，再求Skolem标准型而得到。 还需说明的是，引入Skolem函数，是由于存在量词在全称量词的辖域之内其约束变元的取值完全依赖于全称量词的取值。Skolem函数就反映了这种依赖关系。但注意，Skolem标准型与原公式一般并不等价，例如公式： G=xP(x) 它的Skolem标准型是 G′=P(a) 给出如下的一个解释I D={0，1},a0,P(0)F,P(1)T 则在I下，G=T，而G′=F。 由子句集的求法可以看出，一个子句集中的各子句间为合取关系，且每个个体变元都受全称量词的约束(假定公式中无自由变元，或将自由变元看作常元)。所以，一个公式的子句集也就是该公式的Skolem标准型的另一种表达形式。 有了子句集，就可以通过一个谓词公式的子句集来判断公式的不可满足性。 定理54谓词公式G不可满足当且仅当其子句集S不可满足。 定理54就把证明一个公式G的不可满足性，转化为证明其子句集S的不可满足性。 定义514子句集S是不可满足的，当且仅当其全部子句的合取式是不可满足的。 5.2.2命题逻辑中的归结原理 归结演绎推理是基于一种称为归结原理(也称消解原理，principle of resolution)的推理规则的推理方法。归结原理是由鲁滨逊(J.A.Robinson)于1965年首先提出。它是谓词逻辑中一个相当有效的机械化推理方法。归结原理的出现，被认为是自动推理，特别是定理机器证明领域的重大突破。 定义515设L为一个文字，则称L与瘙綈L为互补文字。 定义516设C1、C2是命题逻辑中的两个子句，C1中有文字L1、C2中有文字L2，且L1与L2互补，从C1、C2中分别删除L1、L2，再将剩余部分析取起来，记构成的新子句为C12，则称C12为C1、C2的归结式(或消解式)，C1、C2称为其归结式的亲本子句，L1、L2称为消解基。 例510设C1=瘙綈P∨Q∨R，C2=瘙綈Q∨S，于是C1、C2的归结式为 瘙綈P∨R∨S 定理55归结式是其亲本子句的逻辑结果。 证明设C1=L∨C′1，C2=瘙綈L∨C′2，C′1、C′2都是文字的析取式，则C1、C2的归结式为C′1∨C′2，因为 C1=C′1∨L=瘙綈C′1→L,C2=瘙綈L∨C′2=L→C′2 所以 C1∧C2=(瘙綈C′1→L)∧(L→C′2)（瘙綈C′1→C′2)=C′1∨C′2 证毕。 由该定理即得下面的推理规则 C1∧C2(C1-{L1})∪(C2-{L2}) 其中C1、C2是两个子句，L1、L2分别是C1、C2中的文字，且L1、L2互补。此规则就是命题逻辑中的归结原理。 例511用归结原理验证常用的推理规则假言推理(分离规则)： P∧(P→Q)Q和拒取式(P→Q)∧瘙綈Q瘙綈P。 证 P∧(P→Q)=P∧(瘙綈P∨Q)Q (P→Q)∧瘙綈Q=(瘙綈P∨Q)∧(瘙綈Q)瘙綈P 类似地可以验证，其他推理规则也可以经消解原理推出。这就是说，用消解原理就可以代替其他所有的推理规则。再加上这个方法的推理步骤比较机械，这就为机器推理提供了方便。 由归结原理可知，如果两个互否的单元子句进行归结，则归结式为空子句，即L∧瘙綈L=□，而另一方面，L∧瘙綈L=F(假)。所以，空子句就是恒假子句，即 □F 归结原理显然是一个很好的推理规则，但一般不使用它直接从前提推导结论，而是通过推导空子句来作间接证明。具体来讲，就是先求出要证的命题公式(谓词公式也一样)的否定式的子句集S，然后对子句集S(一次或多次)使用消解原理，若在某一步推出了空子句，即推出了矛盾，则说明子句集S是不可满足的，从而原否定式也是不可满足的，进而说明原公式是永真的。 为什么说，一旦推出了空子句就说明子句集S是不可满足的呢？这是因为空子句就是F，推出了空子句就是推出了F。但消解原理是推理规则，即正确的推理形式，那么由正确的推理形式推出了F，则说明前提不真，即消解出空子句□的两个亲本子句中至少有一个为假。那么这两个亲本子句如果都是原子句集S中的子句，即说明原子句集S不可满足(因为子句集中各子句间为合取关系)。如果这两个亲本子句不是或不全是S中的子句，那么，它们必定是某次归结的结果，于是，用同样的道理再向上追溯，这样一定会推出原子句集S中至少有一个子句为假，从而说明S不可满足。 实际上，上述分析也可作为定理55的推论。 推论设C1、C2是子句集S的两个子句，C12是它们的归结式，则： (1) 若用C12代替C1、C2，得到新子句集S1，则由S1的不可满足可推出原子句集S的不可满足。即 S1不可满足S不可满足 (2) 若把C12加入S中，得到新子句集S2，则S2与原S同不可满足。即 S2不可满足S不可满足 例512证明子句集{P∨瘙綈Q，瘙綈P，Q}是不可满足的。 证 (1) P∨瘙綈Q (2) 瘙綈P (3) Q (4) 瘙綈Q由(1)(2) (5) □由(3)(4) 图51例513归结演绎树 例513用归结原理证明R是P，(P∧Q)→R，(S∨U)→Q，U的逻辑结果。 证首先把前提条件化为子句形式，再把结论的非也化为子句，由所有子句得到子句集S={P，瘙綈P∨瘙綈Q∨R，瘙綈S∨Q，瘙綈U∨Q，U，瘙綈R}，然后对该子句集施行归结，归结过程用下面的归结演绎树表示(见图51)。由于最后推出了空子句，所以子句集S不可满足，即命题公式P∧(瘙綈P∨瘙綈Q∨R)∧(瘙綈S∨Q)∧(瘙綈U∨Q)∧U∧瘙綈R不可满足，从而得到R是题设前提的逻辑结果。 5.2.3替换与合一 在一阶谓词逻辑中应用消解原理，不像命题逻辑中那样简单，因为谓词逻辑中的子句含有个体变元，这就使寻找含互否文字的子句对的操作变得复杂。例如： C1=P(x)∨Q(x) C2=瘙綈P(a)∨R(y) 直接比较，似乎两者中不含互否文字，但如果用a替换C1中的x，则得到： C′1=P(a)∨Q(a) C′2=瘙綈P(a)∨R(y) 根据命题逻辑中的消解原理，得出C′1和C′2的消解式： C′3=Q(a)∨R(y) 所以，要在谓词逻辑中应用消解原理，则一般需要对个体变元做适当的替换。 定义517一个替换(substitution)是形如{t1/x1,t2/x2,…,tn/xn}的有限集合，其中t1,t2,…,tn是项，称为替换的分子； x1,x2,…,xn是互不相同的个体变元，称为替换的分母； ti不同于xi，xi也不循环地出现在tj(i,j=1,2,…,n)中； ti/xi表示用ti替换xi。若t1,t2,…,tn都是不含变元的项(称为基项)时，该替换称为基替换； 没有元素的替换称为空替换，记作ε，它表示不做替换。 例如： {a/x，g(y)/y，f(g(b))/z}就是一个替换，而{g(y)/x，f(x)/y}则不是一个替换，因为x与y出现了循环替换。 下面将项、原子公式、文字、子句等统称为表达式，没有变元的表达式称为基表达式，出现在表达式E中的表达式称为E的子表达式。 定义518设θ={t1/x1,…,tn/xn}是一个替换，E是一个表达式，把对E施行替换θ，即把E中出现的个体变元xj(1≤j≤n)都用tj替换，记为Eθ，所得的结果称为E在θ下的例(Instance)。 定义519设θ={t1/x1,…，tn/xn}，λ={u1/y1,…，um/ym}是两个替换，则将集合{t1λ/x1,…,tnλ/xn,u1/y1,…,um/ym}中凡符合下列条件的元素删除： (1) tiλ/xitiλ=xi (2) ui/yiyi∈{x1,…,xn} 如此得到的集合仍然是一个替换，该替换称为θ与λ的复合或乘积，记为θ·λ。 例514设θ={f(y)/x，z/y}，λ={a/x，b/y，y/z}，于是， {t1λ/x1，t2λ/x2，u1/y1，u2/y2，u3/y3}={f(b)/x，y/y，a/x，b/y，y/z} 从而 θ·λ={f(b)/x，y/z} 可以证明，替换的乘积满足结合律，即 (θ·λ)·u=θ·(λ·u) 定义520设S={F1,F2,…,Fn}是一个原子谓词公式集，若存在一个替换θ，可使F1θ=F2θ=…=Fnθ，则称θ为S的一个合一(unifier)，称S为可合一的。 定义521设σ是原子公式集S的一个合一，如果对S的任何一个合一θ，都存在一个替换λ，使得 θ=σ·λ 则称σ为S的最一般合一(most general unifier，MGU)。 例515设S=［P(u，y，g(y))，P(x，f(u)，z)］，S有一个最一般合一 σ={u/x，f(u)/y，g(f(u))/z} 对S的任一合一，例如 θ={a/x,f(a)/y，g(f(a))/z，a/u} 存在一个替换 λ={a/u} 使得 θ=σ·λ 可以看出，如果能找到一个公式集的合一，特别是最一般合一，则可使互否文字的形式结构完全一致起来，进而达到消解的目的。如何求一个公式集的最一般合一？有一个算法，可以求任何可合一公式集的最一般合一。为了介绍这个算法，先引入差异集的概念。 定义522设S是一个非空的具有相同谓词名的原子公式集，从S中各公式的左边第一个项开始，同时向右比较，直到发现第一个不都相同的项为止，用这些项的差异部分组成一个集合，这个集合就是原公式集S的一个差异集。 例516设S={P(x，y，z)，P(x，f(a)，h(b))}，则不难看出，S有两个差异集 D1={y，f(a)} D2={z，h(b)} 设S为一非空有限具有相同谓词名的原子谓词公式集，下面给出求其最一般合一的算法。 合一算法(Unification algorithm) (1) 置k=0，Sk=S，σk=ε。 (2) 若Sk只含有一个谓词公式，则算法停止，σk就是要求的最一般合一。 (3) 求Sk的差异集Dk。 (4) 若Dk中存在元素xk和tk，其中xk是变元，tk是项且xk不在tk中出现，则置Sk+1=Sk{tk/xk}，σk+1=σk·{tk/xk}，k=k+1，然后转步骤(2)。 (5) 算法停止，S的最一般合一不存在。 5.2.4谓词逻辑中的归结原理 定义523设C1、C2是两个无相同变元的子句，L1、L2分别是C1、C2中的两个文字，如果L1和L2有最一般合一σ，则子句(C1σ-{L1σ})∪(C2σ-{L2σ})称作C1和C2的二元归结式(或二元消解式)，C1和C2称作归结式的亲本子句，L1和L2称作消解文字。 例517设C1=P(x)∨Q(x),C2=瘙綈P(a)∨R(y)，求C1、C2的归结式。 解取L1=P(x),L2=瘙綈P(a)，则L1与瘙綈L2的最一般合一σ={a/x}，于是， (C1σ-{L1σ})∪(C2σ-{L2σ}) =({P(a),Q(a)}-{P(a)})∪({瘙綈P(a),R(y)}-{瘙綈P(a)}) ={Q(a)，R(y)} =Q(a)∨R(y) 所以，Q(a)∨R(y)是C1和C2的二元归结式。 例518设C1=P(x，y)∨瘙綈Q(a)，C2=Q(x)∨R(y),求C1、C2的归结式。 解由于C1、C2中都含有变元x、y，所以需先对其中一个进行改名，方可归结(归结过程是显然的，故从略)。还需说明的是，如果在参加归结的子句内部含有可合一的文字，则在进行归结之前，也应对这些文字进行合一，从而使子句达到最简。例如，设有两个子句： C1=P(x)∨P(f(a))∨Q(x) C2=瘙綈P(y)∨R(b) 可见，在C1中有可合一的文字P(x)与P(f(a))，那么，取替换θ={f(a)/x}［这个替换也就是P(x)和P(f(a))的最一般合一］，则得 C1θ=P(f(a))∨Q(f(a)) 现在再用C1θ与C2进行归结，从而得到C1与C2的归结式 Q(f(a))∨R(b) 定义524如果子句C中，两个或两个以上的文字有一个最一般合一σ，则Cσ称为C的因子，如果Cσ是单元子句，则Cσ称为C的单因子。 例519设C=P(x)∨P(f(y))∨瘙綈Q(x),令σ={f(y)/x}，于是Cσ=P(f(y))∨瘙綈Q(f(y))是C的因子。 定义525子句C1、C2的消解式，是下列二元消解式之一： (1) C1和C2的二元消解式； (2) C1和C2的因子的二元消解式； (3) C1的因子和C2的二元消解式； (4) C1的因子和C2的因子的二元消解式。 定理56谓词逻辑中的消解式是它的亲本子句的逻辑结果。 由此定理即得谓词逻辑中的推理规则 C1∧C2(C1σ-{L1σ})∪(C2σ-{L2σ}) 其中，C1、C2是两个无相同变元的子句，L1、L2分别是C1、C2中的文字，σ为L1与瘙綈L2的最一般合一。此规则称为谓词逻辑中的消解原理(或归结原理)。 例520求证G是A1和A2的逻辑结果。 A1： x(P(x)→(Q(x)∧R(x))) A2： x(P(x)∧S(x)) G： x(S(x)∧R(x)) 证用反证法，即证明A1∧A2∧瘙綈G不可满足。首先求得子句集S： (1) 瘙綈P(x)∨Q(x) (2) 瘙綈P(y)∨R(y)（A1） (3) P(a) (4) S(a)（A2） (5) 瘙綈S(z)∨瘙綈R(z)(瘙綈G)S 然后应用消解原理，得 (6) R(a)［(2)，(3),σ1={a/y}］ (7) 瘙綈R(a)［(4)，(5),σ2={a/z}］ (8) □［(6)，(7)］ 所以，S是不可满足的，从而G是A1和A2的逻辑结果。 例521设已知： (1) 能阅读者是识字的。 (2) 海豚不识字。 (3) 有些海豚是很聪明的。 试证明： 有些聪明者并不能阅读。 证首先，定义如下谓词。 R(x)： x能阅读。 L(x)： x识字。 I(x)： x是聪明的。 D(x)： x是海豚。 然后把上述各语句翻译为谓词公式： (1) x(R(x)→L(x)) (2) x(D(x)→瘙綈L(x)) (3) x(D(x)∧I(x))已知条件 (4) x(I(x)∧瘙綈R(x))需证结论 求题设与结论否定的子句集，得 (1) 瘙綈R(x)∨L(x) (2) 瘙綈D(y)∨瘙綈L(y) (3) D(a) (4) I(a) (5) 瘙綈I(z)∨R(z) 归结得 (6) R(a)由(5)(4)，{a/z} (7) L(a)由(6)(1)，{a/x} (8) 瘙綈D(a)由(7)(2)，{a/y} (9) □由(8)(3) 图52例521的归结演绎树 这个归结过程的演绎树如图52所示。 由以上例子可以看出，谓词逻辑中的消解原理也可以代替其他推理规则。 上面通过推导空子句证明了子句集的不可满足性，因此，存在问题： 对于任一不可满足的子句集，是否都能通过归结原理推出空子句呢？回答是肯定的。 定理57(归结原理的完备性定理)如果子句集S是不可满足的，那么必存在一个由S推出空子句□的消解序列(该定理的证明要用到Herbrand定理，故从略)。 5.3应用归结原理求取问题答案 归结原理除了能用于对已知结果的证明外，还能用于对未知结果的求解，即能求出问题的答案来。请看下例。 例522已知： (1) 如果x和y是同班同学，则x的老师也是y的老师。 (2) 王先生是小李的老师。 (3) 小李和小张是同班同学。 问： 小张的老师是谁？ 解设谓词T(x，y)表示x是y的老师，C(x，y)表示x与y是同班同学，则已知可表示成如下的谓词公式 F1： xyz(C(x，y)∧T(z，x)→T(z，y)) F2： T(Wang，Li) F3： C(Li，Zhang) 为了得到问题的答案，先证明小张的老师是存在的，即证明公式 G： xT(x，Zhang) 于是，求F1∧F2∧F3∧→G的子句集如下： (1) 瘙綈C(x，y)∨瘙綈T(z，x)∨T(z，y) (2) T(Wang，Li) (3) C(Li，Zhang) (4) 瘙綈T(u，Zhang) 归结演绎，得 (5) 瘙綈C(Li，y)∨T(Wang，y)由(1)(2)，{Wang/z，Li/x} (6) 瘙綈C(Li，Zhang)由(4)（5)，{Wang/u，Zhang/y} (7) □由(3)(6) 这说明，小张的老师确实是存在的。那么，为了找到这位老师，我们给原来的求证谓词的子句再增加一个谓词ANS(u)。于是，得到 (4)′ 瘙綈T(u，Zhang)∨ANS(u) 现在，用(4)′代替(4)，重新进行归结，则得 (5)′ 瘙綈C(Li，y)∨T(Wang，y)由(1)(2) (6)′ 瘙綈C(Li，Zhang)∨ANS(Wang)由(4)′(5)′ (7)′ ANS(Wang)由(3)(6)′ 可以看出，归结到这一步，求证的目标谓词已被消去，即求证已成功，但还留下了谓词ANS(Wang)。由于该谓词中原先的变元与目标谓词T(u，Zhang)中的一致，所以，其中的Wang也就是变元u的值。这样，就求得了小张的老师，也就是王老师。 上例虽然是一个很简单的问题，但它给了我们一个利用归结原理求取问题答案的方法，那就是： 先为待求解的问题找一个合适的求证目标谓词； 再给增配(以析取形式)一个辅助谓词，且该辅助谓词中的变元必须与对应目标谓词中的变元完全一致； 然后进行归结，当某一步的归结式刚好只剩下辅助谓词时，辅助谓词中原变元位置上的项(一般是常量)就是所求的问题答案。 需说明的是，辅助谓词(如此题中的ANS)是一个形式谓词，其作用仅是提取问题的答案，因而也可取其他谓词名。有些文献中就用需求证的目标谓词。如对上例，就取T(u，Zhang)为辅助谓词。 例523设有如下关系： (1) 如果x是y的父亲，y又是z的父亲，则x是z的祖父。 (2) 老李是大李的父亲。 (3) 大李是小李的父亲。 问： 上述人员中谁和谁是祖孙关系？ 解先把上述前提中的3个命题符号化为谓词公式： F1： xyz(F(x，y)∧F(y，z)→G(x，z)) F2： F(Lao，Da) F3： F(Da，Xiao) 并求其子句集如下： (1) 瘙綈F(x，y)∨瘙綈F(y，z)∨G(x，z) (2) F(Lao，Da) (3) F(Da，Xiao) 设求证的公式为 G： xyG(x，y)(即存在x和y，x是y的祖父) 把其否定化为子句形式再析取一个辅助谓词GA(x，y)，得 (4) 瘙綈G(u，v)∨GA(u，v) 对(1)~(4)进行归结，得 (5) 瘙綈F(Da，z)∨G(Lao，z)由(1)(2)，{Lao/x，Da/y} (6) G(Lao，Xiao)由(3)(5)，{Xiao/z} (7) GA(Lao，Xiao)由(4)(6)，{Lao/u，Xiao/v} 所以，上述人员中，老李是小李的祖父。 5.4归结策略* 5.4.1问题的提出 前面介绍了归结原理及其应用，但那些归结推理都是用人工实现的。而人们研究归结推理的目的主要是为了更好地实现机器推理，或者说自动推理。那么，现在就存在问题： 归结原理如何在机器上实现？ 把归结原理在机器上实现，就意味着用算法描述归结原理，然后编制程序，在计算机上运行。下面给出一个实现归结原理的一般性算法： (1) 将子句集S置入CLAUSES表。 (2) 若空子句NIL在CLAUSES中，则归结成功，结束。 (3) 若CLAUSES表中存在可归结的子句对，则归结之，并将归结式并入CLAUSES表，转步骤(2)。 (4) 归结失败，退出。 可以看出，这个算法并不复杂，但问题是在其步骤(3)中应该以什么样的次序从已给的子句集S出发寻找可归结的子句对进行归结呢？ 一种简单而直接的想法就是逐个考察CLAUSES表中的子句，穷举式地进行归结。可采用这样的具体做法： 第一轮归结先让CLAUSES表(即原子句集S)中的子句两两见面进行归结，将产生的归结式集合记为S1，再将S1并入CLAUSES得CLAUSES=S∪S1； 下一轮归结时，又让新的CLAUSES即S∪S1与S1中的子句互相见面进行归结，并把产生的归结式集合记为S2，再将S2并入CLAUSES； 在再一轮归结时，又让S∪S1∪S2与S2中的子句进行归结……如此进行，直到某一个Sk中出现空子句□为止。下面举例说明。 例524设有如下的子句集S，用上述的穷举算法归结如下。 S： (1) P∨Q (2) 瘙綈P∨Q (3) P∨瘙綈Q (4) 瘙綈P∨瘙綈Q S1： (5) Q［(1)，(2)］ (6) P［(1)，(3)］ (7) Q∨瘙綈Q［(1)，(4)］ (8) P∨瘙綈P［(1)，(4)］ (9) Q∨瘙綈Q［(2)，(3)］ (10) P∨瘙綈P［(2)，(3)］ (11) 瘙綈P［(2)，(4)］ (12) 瘙綈Q［(3)，(4)］ S2： (13) P∨Q［(1)，(7)］ (14) P∨Q［(1)，(8)］ (15) P∨Q［(1)，(9)］ (16) P∨Q［(1)，(10)］ (17) Q［(1)，(11)］ (18) P［(1)，(12)］ (19) Q［(2)，(6)］ (20) 瘙綈P∨Q ［(2)，(7)］ (21) 瘙綈P∨Q［(2)，(8)］ (22) 瘙綈P∨Q［(2)，(9)］ (23) 瘙綈P∨Q［(2)，(10)］ (24) 瘙綈P［(2)，(12)］ (25) P［(3)，(5)］ (26) P∨瘙綈Q ［(3)，(7)］ (27) P∨瘙綈Q［(3)，(8)］ (28) P∨瘙綈Q［(3)，(9)］ (29) P∨瘙綈Q［(3)，(10)］ (30) 瘙綈Q［(3)，(11)］ (31) 瘙綈P［(4)，(5)］ (32) 瘙綈Q［(4)，(6)］ (33) 瘙綈P∨瘙綈Q［(4)，(7)］ (34) 瘙綈P∨瘙綈Q［(4)，(8)］ (35) 瘙綈P∨瘙綈Q［(4)，(9)］ (36) 瘙綈P∨瘙綈Q［(4)，(10)］ (37) Q［(5)，(7)］ (38) Q［(5)，(9)］ (39) □［(5)，(12)］ 可以看出，这个归结方法无任何技巧可言，只是一味地穷举式归结。因而对于如此简单的问题，计算机推导了35步，即产生35个归结式，才导出了空子句。那么，对于一个规模较大的实际问题，其时空开销就可想而知了。事实上，这种方法一般会产生许多无用的子句。这样，随着归结的进行，CLAUSES表将会越来越庞大，以至于机器不能容纳。同时，归结的时间消耗也是一个严重问题。 那么，怎样归结才能高效地推出空子句NIL呢？研究表明，要提高归结的效率，就必须运用一定的技巧，即所谓归结策略。例如，对于例524中的问题，若运用一定的策略，则仅用3步就可以解决问题。 事实上，归结反演的过程，就是一个在子句空间中搜索(空子句)的过程。因此，要用归结原理实现机器推理，一个重要的问题就是要赋予机器一定的搜索策略，即归结策略。这就是说，要让计算机进行归结演绎推理，仅有归结原理还不够，还必须研究归结策略。归结策略有哪些？下面将介绍几种。 需说明的是，上述的归结方法实际上是一种广度优先的按层次进行归结的方法。所以，一般也把它说成是一种归结策略，称之为广度优先策略，也可称为水平浸透法。 5.4.2常用的归结策略 1. 删除策略 定义526设C1、C2是两个子句，若存在替换θ，使得C1θC2，则称子句C1类含C2。 例如： P(x)类含P(a)∨Q(y)(只需取θ={a/x}) Q(y)类含P(x)∨Q(y)(θ=ε) P(x)类含P(x)，P(x)类含P(a)，P类含P，P类含P∨R P(a，x)∨P(y，b)类含P(a，b)(取θ={b/x，a/y}) 删除策略： 在归结过程中可随时删除以下子句： (1) 含有纯文字的子句。 (2) 含有永真式的子句。 (3) 被子句集中别的子句类含的子句。 所谓纯文字，是指那些在子句集中无补的文字。例如下面的子句集 {P(x)∨Q(x，y)∨R(x),瘙綈P(a)∨Q(u，v),瘙綈Q(b，z),瘙綈P(w)} 其中的文字R(x)就是一个纯文字。 删除含有纯文字的子句，是因为在归结时纯文字永远不会被消去，因而用包含它的子句进行归结不可能得到空子句。删除永真式是因为永真式对子句集的不可满足性不起任何作用。删除被类包含的子句是因为它被类含它的子句所逻辑蕴涵，故它已是多余的。 例525对例524中的子句集使用删除策略。可以看出，这时原归结过程中产生的有些归结式是永真式(如(7)(8)(9)(10))，有些被前面已有的子句所类含(如(17)(18)等，重复出现可认为是一种类含)，因此，它们可被立即删除。这样就导致它们的后裔将不可能出现。其归结步骤可简化为： (1) P∨Q (2) 瘙綈P∨Q (3) P∨瘙綈Q (4) 瘙綈P∨瘙綈Q (5) Q［(1)，(2)］ (6) P［(1)，(3)］ (7) 瘙綈P［(2)，(4)］ (8) 瘙綈Q［(3)，(4)］ (9) □［(5)，(8)］ 其实，上述归结还可以进一步简化为： (5) Q［(1)，(2)］ (6) 瘙綈Q［(3)，(4)］ (7) □［(5)，(6)］ 这是因为，(5)出现后，由于它就类含了(1)(2)，所以可将(1)和(2)删除。 同理，当(6)出现时，可将(3)(4)删除。这样，下面也只能是(5)(6)归结了。 例526对下面的子句集S，用宽度优先策略与删除策略相结合的方法进行消解。 S： (1) P(x)∨Q(x)∨瘙綈R(x) (2) 瘙綈Q(a) (3) 瘙綈R(a)∨Q(a) (4) P(y) (5) 瘙綈P(z)∨R(z) 可以看出，(4)类含了(1)，所以先将(1)删除。由剩下的4个子句归结得： S1： (6) 瘙綈R(a)［(2),(3)］ (7) 瘙綈P(a)∨Q(a)［(3)，(5)，{a/z}］ (8) R(z)［(4)，(5)，{z/y}］ (6)出现后(3)可被删除，所以，第二轮归结在(2)、(4)、(5)、(6)、(7)、(8)间进行。其中(2)、(4)、(5)间的归结不必再重做，于是得 S2： (9) 瘙綈P(a)［(2),(7)］ (10) Q(a)［(4),(7),{a/y}］ (11) 瘙綈P(a)［(5)，(6)，{a/z}］ (12) □［(6)，(8)，{a/z}］ 删除策略有如下特点： （1） 删除策略的思想是及早删除无用子句，以避免无效归结，缩小搜索规模； 尽量使归结式朝“小”(即元数少)方向发展，从而尽快导出空子句。 （2） 删除策略是完备的。即对于不可满足的子句集，使用删除策略进行归结，最终必导出空子句□。 定义527一个归结策略是完备的，如果对于不可满足的子句集，使用该策略进行归结，最终必导出空子句□。 2. 支持集策略 支持集策略： 每次归结时，两个亲本子句中至少要有一个是目标公式否定的子句或其后裔。这里的目标公式否定的子句集即为支持集。 例527设有子句集 S={瘙綈I(x)∨R(x)，I(a)，瘙綈R(y)∨瘙綈L(y)，L(a)} 其中，子句瘙綈I(x)∨R(x)是目标公式否定的子句。 用支持集策略归结如下： S： (1) 瘙綈I(x)∨R(x) (2) I(a) (3) 瘙綈R(y)∨瘙綈L(y) (4) L(a) S1： (5) R(a)由(1)(2)，{a/x} (6) 瘙綈I(x)∨瘙綈L(x)由(1)(3)，{x/y} S2： (7) 瘙綈L(a)由(5)(3)，{a/y} (8) 瘙綈L(a)由(6)(2)，{a/x} (9) 瘙綈I(a)由(6)(4)，{a/x} (10) □由(7)(4) 支持集策略有如下特点： （1） 这种策略的思想是尽量避免在可满足的子句集中做归结，因为从中导不出空子句。而求证公式的前提通常是一致的，所以，支持集策略要求在归结时从目标公式否定的子句出发进行归结。所以，支持集策略实际是一种目标制导的反向推理。 （2） 支持集策略是完备的。 3. 线性归结策略 线性归结策略： 在归结过程中，除第一次归结可都用给定的子句集S中的子句外，其后的各次归结至少要有一个亲本子句是上次归结的结果。 例528对例527中的子句集，用线性归结策略归结。 (1) 瘙綈I(x)∨R(x) (2) I(a) (3) 瘙綈R(y)∨瘙綈L(y) (4) L(a) (5) R(a)由(1)(2)，{a/x} (6) 瘙綈L(a)由(5)(3)，{a/y} (7) □由(6)(4) 线性归结策略的特点是： 不仅它本身是完备的，高效的，而且还与许多别的策略兼容。例如在线性归结中可同时采用支持集策略或输入策略。 4. 输入归结策略 输入归结策略： 每次参加归结的两个亲本子句，必须至少有一个是初始子句集S中的子句。 输入归结策略的特点是：  输入归结策略实际是一种自底向上的推理，它有相当高的效率。  输入归结是不完备的。例如子句集 S={P∨Q，瘙綈P∨Q，P∨瘙綈Q，瘙綈P∨瘙綈Q} 是不可满足的。用输入归结都不能导出空子句，因为最后导出□的子句必定都是单文字子句，它们不可能在S中。 输入归结往往同线性归结配合使用，组成所谓线性输入归结策略。其进一步还可以与支持集策略结合。 5. 单元归结策略 单元归结策略： 在归结过程中，每次参加归结的两个亲本子句中必须至少有一个是单元子句。 单元归结策略的特点：  单元归结的思想是，用单元子句归结可使归结式含有较少的文字，因而有利于尽快逼近空子句。  单元归结也是一种效率高但不完备的策略。 单元归结和输入归结虽都不完备，但应用它们可以证明相当广泛的一类定理，因此，它们不失为好的归结策略。另外，理论研究还表明： 对不可满足的子句集S，可用单元归结导出空子句当且仅当可用输入归结导出空子句。 单纯使用单元归结有时可能无法归结(当无单元子句时)。因此，一般是将单元归结的条件放宽，变为优先对单元子句进行归结。这种策略称为单元优先策略。 6. 祖先过滤形策略 祖先过滤形策略： 参加归结的两个子句，要么至少有一个是初始子句集中的子句； 要么一个是另一个的祖先(或者说一个是另一个的后裔)。 5.4.3归结策略的类型 除了上面介绍的一些常用的归结策略，人们还提出了许多别的策略，如锁归结、语义归结、加权策略、模型策略等。 锁归结的思想是： 用数字1、2、3……对各子句中的文字进行编号，使互不相同的文字或相同文字的不同出现具有不同的编号，这种编号称为文字的锁，如1P∨3Q和5P∨9P中的1、3、5、9都是锁。这样，归结就可以用锁来控制。具体做法是： 每次归结，参加归结的文字必须分别是所在子句中编号最小者。例如，有子句1P∨2Q和3瘙綈P∨4瘙綈Q，则只能对P、瘙綈P作归结。 语义归结的基本思想是将子句集S中的子句分成两组，只考虑组间子句的归结。加权策略是对子句或其中的项赋予相应的权值，以反映子句或项在实际问题中的某种程度，这样，归结就可以用权值来控制，如给出某种顺序或限制。 归结策略很多，归纳起来，大致可以分为3类： (1) 简化性策略。 这种策略的思想是尽量简化子句和子句集，以减少和避免无效归结。如删除策略就是简化策略。然而，简化策略在使用时，也要付出一定的开销，如要不断地做包含检验或真值计算。这又是它的缺点。 (2) 限制性策略。 前面所介绍的策略多数都是限制性策略。如支持集策略、线性策略、输入策略、单元策略、祖先过滤策略、语义归结等。限制性策略的思想是尽量缩小搜索范围，以提高搜索效率。 (3) 有序性策略。 有序性策略的思想是给子句安排一定的顺序，以便能尽快地推出空子句。单元优先策略、加权策略以及锁归结等都是有序性归结策略。 有了归结策略后，从本节开始所给的归结反演一般算法可改为： (1) 将子句集S置入CLAUSES表。 (2) 若空子句NIL在CLAUSES中，则归结成功，结束。 (3) 按某种策略在CLAUSES表中寻找可归结的子句对，若存在则归结之，并将归结式并入CLAUSES表，转步骤(2)。 (4) 归结失败，退出。 5.5归结反演程序举例* 下面给出一个可用于命题逻辑归结反演的PROLOG示例程序。 prove(F，S): -union(F，S，SY)，proof(SY). union(［］，Y，Y). union(［X|XR］，Y，Z): -member(X，Y)，!，union(XR，Y，Z). union(［X|XR］，Y，［X|ZR］): -union(XR，Y，ZR). proof(［SH|ST］): -resolution(SH，ST，［］)，!. proof(［SH|ST］): -resolution(SH，ST，NF)，proof(［NF，SH|ST］). resolution(SH,［STH|ST］,NF):-resolve(SH,STH,NF1),NF1=SH,!，resolution(SH，ST，NF). resolution(SH，［STH|ST］，NF): -resolve(SH，STH，NF)，print(SH，STH，NF). resolve(［］,_，［］): -!. resolve(［F|FR］，SF，FR): -not(F=no)，invert(F，IF)，IF=SF，!. resolve(［F|FR］，SF，NF): -not(F=no)，invert(F，IF)，member(IF，SF)，!， pack(F，FR，SF，NF). resolve(［F|FR］,SF,NF):-not(F=no),!,resolve(FR,SF,NF1)，pack((［］，［F］，［NF1］，NF). resolve(F，SF，［］): -invert(F，IF)，IF=SF，!. resolve(F，SF，NF): -invert(F，IF)，member(IF，SF)，!，pack(F，［］，SF，NF). resolve(F,_，F). invert(X，［no，X］): -atom(X). invert(［no，X］，X): -atom(X). member(X，［X|_］): -!. member(X，［_|Y］): -member(X，Y). pack(A，X，Y，Z): -combine(A，X，Y，［Z|［］］)，!. pack(A，X，Y，Z): -combine(A，X，Y，Z). combine(A,X,Y,Z): -union(X，Y，Z1)，delete(A，Z1，Z2)，invert(A，IA)，delete(IA，Z2，Z). delete(_，［］，［］). delete(E，［E|ER］，R): -!，delete(E，ER，R). delete(E，［X|XR］，［X|R］): -delete(E，XR，R). print(F，S，R): -write(F)，write(′，′)，write(S)，write("?")，write(R)，nl. 该程序把子句用表来表示。例如： 子句瘙綈P∨Q，表示为［［not，p］，q］。子句集用子句表表示。例如： 子句集{瘙綈P∨Q，R∨S，U}，则表示为 ［［［not，p］，q］，［r，s］，u］ 该程序的目标子句是prove(F，S)。其中，S为前提，F为要证明的结论的否定。程序运行时，谓词union(F，S，FS)首先把待证结论的否定子句F与前提子句S合并为FS。接着，谓词proof(FS)对子句集FS进行归结反演，试图推出空子句［］。proof又调用谓词resolution进行归结。proof的第一个子句是归结反演的终结条件； 第二个子句是归结反演的递归操作。 resolution(SH，ST，NF)谓词实现具体的归结操作。其中SH是从子句集FS中分离出的一个子句，它作为一个双亲子句； ST为去掉SH后的子句集； NF是SH与ST中子句产生的归结式。 resolution的第一个子句处理ST子句集中的第一个子句STH不能与SH归结的情况，将引起resolution的递归操作。在这里，resolve子句把SH放入NF，于是resolution子句根据NF1=SH知道STH不能与SH组成互补对，便对剩下部分(去掉STH以后的表尾)进行递归处理。resolution的第二个子句处理ST子句集中的第一个子句STH能与SH归结的情况，这时将SH与STH的归结式放入NF。接着由print(SH，STH，NF)输出这一步的归结推理。 resolve(SH，STH，NF)谓词的作用是检查SH和STH是否为可归结的双亲子句。resolve共有7个子句。第一个子句是终止条件。第二至第四个子句处理SH为非单项析取式的情况，它们对SH从左到右依次查看每一个单项析取式，看是否在STH中存在它的否定，若存在则进行归结，若不存在则进行递归处理。其中，第二个子句处理STH为单项析取式的情况，第三个子句处理STH为非单项析取式的情况，第四个子句处理STH中不存在SH中的单项析取式的否定的情况。第五、第六个子句处理SH为单项析取式的情况，其中第五个子句处理STH也为单项析取式的情况，第六个子句处理STH为非单项析取式的情况。这两个子句直接判断SH能否与STH归结，子句5归结结果为［］，即产生矛盾； 子句6产生归结式NF。第七个子句处理SH不能与STH归结的情况。 pack(F，FR，SF，NF)谓词的功能是将子句［F|FR］和SF归结，产生归结式NF，其中F是引起归结的项。pack的第一个子句将删除归结式中可能多余的括号［］。如由［p，q］和［not，p］产生的归结式［q］便被改为q。pack的第二个子句调用combine来删除形如L、瘙綈L的互补对，并确保在归结式中没有重复的元素。 invert(F，IF)谓词的功能是将F取否定放在IF中。 现在用这个程序证明瘙綈P∨瘙綈U是Q∨瘙綈P，R∨瘙綈Q，S∨瘙綈R和瘙綈U∨瘙綈S的逻辑结论。则有目标 ?-prove(［p，u］，［［q，［no，p］］，［r，［no，q］］，［s，［no，r］］，［［no，u］，［no，s］］］). 对此目标，程序的运行结果为： p，［q，［not，p］］q q，［r，［not，q］］r r，［s，［not，r］］s s，［［not，u］，［not，s］［not，u］ ［not，u］，u［］ yes 5.6Horn子句逻辑与逻辑程序设计语言* 5.6.1子句的蕴涵表示形式 我们知道，原子公式及其否定称为文字，现在把前者称为正文字，后者称为负文字。例如子句P(x)∨瘙綈Q(x，y)中P(x)为正文字，瘙綈Q(x，y)为负文字。子句是若干文字的析取，析取词又满足交换律，所以对于任一个子句，总可以将其表示成如下形式 瘙綈Q1∨…∨瘙綈Qn∨P1∨…∨Pm(51) 其中，Pi，瘙綈Qj皆为文字。可以看出，式(51)进一步可变形为 Q1∧Q2∧…∧Qn→P1∨P2∨…∨Pm(52) 式(52)为一个蕴涵式，如果约定蕴涵式前件的文字之间恒为合取关系，而蕴涵式后件的文字恒为析取关系，那么式(52)又可以改写为 Q1，Q2，…，Qn→P1，P2，…，Pm(53) 由于技术上的原因，又将式(53)改写为 P1，P2，…，Pm←Q1，Q2，…，Qn(54) 作为特殊情形，当m=0时式(54)变为 ←Q1，Q2，…，Qn(54′) 它相当于瘙綈(Q1∧Q2∧…∧Qn)； 当n=0时，式(54)变为 P1，P2，…，Pm←(54″) 它相当于P1∨P2∨…∨Pm。 这样，对于任一子句，总可以把它表示成式(54)的形式。子句的这种表示形式称为子句的蕴涵表示形式。例如，子句瘙綈P(x)∨Q(x，y)∨瘙綈R(y)的蕴涵表示形式为： Q(x，y)←P(x)，R(y) 可以看出，对于子句的蕴涵表示形式，消解过程变为： 从其中一个子句的←号左侧与另一个子句的←号右侧(或从其中一个子句的←号右侧与另一个子句的←号左侧)的文字中寻找可合一文字对，然后消去它们，并把其余的左部(即←号的左侧)文字合并，作为消解式的左部，其余的右部文字合并，作为消解式的右部。 例如，子句Q1(x)，Q2(x)←P1(x)，P2(x)和P1(y)←R1(y)，R2(y)的归结式为 Q1(x)，Q2(x)←R1(x)，R2(x)，P2(x) 一般地，这种蕴涵型子句的归结过程可表示如下： 设子句 C： P1，…，Pm←Q1，…，Qn 和 C′： P′1，…，P′s←Q′1，…，Q′t 中有Pi与Q′j(或Qi与P′j)可合一，σ为它们的MGU，则C与C′的归结式为 P1σ，…，Pi-1σ，Pi+1σ，…，Pmσ，P′1σ，…，P′sσ← Q1σ，…，Qnσ，Q′1σ，…，Q′j-1σ，Q′j+1σ，…，Q′tσ 或 P1σ，…，Pmσ，P′1σ，…，P′j-1σ，P′j+1σ，…，P′sσ← Q1σ，…，Qi-1σ，Qi+1σ，…，Qnσ，Q′1σ，…，Q′tσ 5.6.2Horn子句逻辑与计算机程序语言 定义528至多含有一个正文字的子句称为Horn(有些文献中译为“霍恩”)子句(因逻辑学家Alfred Horn首先研究它而得名)。 由定义，蕴涵型Horn子句有以下3种： (1) P←Q1，Q2，…，Qm称为条件子句，P称为头部或结论 (2) P←称为无条件。 (3) ←Q1，Q2，…，Qm称为目标子句，Qi称为子目标。 可以看出，Horn子句形式简明，逻辑意义清晰。更重要的是Horn子句的消解过程可与计算机程序的执行过程统一起来。 例529证明P(a，c)是下面子句集{(1)，(2)，(3)，(4)}的逻辑结论。 证 (1) P(x，z)←P1(x，y)，P2(y，z) (2) P1(u，v)←P11(u，v) (3) P11(a，b)← (4) P2(b，c)←(前提) (5) ←P(a，c)(目标子句) 从目标子句出发，采用线性归结： (6) ←P1(a，y)，P2(y，c)［(5)，(1)，{a/x，c/z}］ (7) ←P11(a，y)，P2(y，c)［(6)，(2)，{a/u，y/v}］ (8) ←P2(b，c)［(7)，(3)，{b/y}］ (9) □［(8)，(4)］ 仔细考察以上归结过程，可以看出，上述归结过程中除最后一次外，每次产生的归结式都是目标子句； 归结过程实际是对第一个目标的求解而导致了一连串目标求解； 而目标求解的过程类似于计算机程序执行中的过程调用。事实上，如果用程序的眼光去看，则子句(1)和(2)就都是“过程”。例如(1)中P就是过程名，(5)和(1)消解就是对过程P的调用，而P的过程体为{P1(x，y)，P2(y，z)}，从而又引起了对子过程P1、P2的调用，这样层层调用下去，子句(3)、(4)提供了过程出口。所以，子句(5)其实就相当于主程序，它包含一个过程调用。也就是说，Horn子句与程序中的过程，基于Horn子句集的线性归结与程序的执行，不谋而合。 可见，完全可以把Horn子句逻辑作为一种计算机程序语言。这样，每一个Horn子句就是该语言中的语句，一个Horn子句的有限集合就是一个程序。这种用Horn子句组成的程序被称为逻辑程序。那么，用Horn子句实现的语言就是逻辑程序设计语言。显然，PROLOG语言就是以Horn子句逻辑为基础的逻辑程序设计语言。这也就是称其为逻辑程序设计语言的原因。 PROLOG程序的运行是一种从问题语句(目标语句)开始的线性归结过程。每次归结时，子目标的选择顺序是从左到右，新子目标的插入顺序是插入子目标队列的左端，匹配子句的顺序是自上而下，搜索空子句的策略是深度优先，推理方式是反向推理，且有回溯机制。PROLOG程序的这种归结方法称为基于Horn子句的SLD(Linear resolution with Selection function for Definite clause)归结，也称为SLD反驳消解法。 上面介绍了谓词逻辑中的归结演绎推理。归结演绎虽然是一种有效的机器推理方法，但它仍存在不少问题。例如，归结策略仍然不能彻底解决大量无用归结式产生的问题。再从其本身来看，谓词公式的子句表达，掩盖了蕴涵词所表示的因果关系，使前提与结论混在一起，不便于在推理中使用启发式信息，知识表示的可读性也差。所以，这就导致人们又对非归结演绎推理进行研究。非归结演绎推理也取有不少成果，比较著名的有Bledsoe自然演绎法、基于规则的演绎推理、王浩算法等。由篇幅所限，这里不再介绍。 延伸学习导引 本章的内容属于自动推理的范畴，在本章的基础上可参阅自动推理方面的著作继续学习。具体来讲，延伸学习的内容包括各种非经典(或非标准)逻辑及其推理。如模态逻辑、时态逻辑、动态逻辑、真度逻辑、软语言真值逻辑、多值逻辑、多类逻辑和非单调逻辑等。除了基于各种逻辑的推理外，还有约束推理、定性推理、范例推理、并行推理、默认推理等。 习题5 1. 将下列句子用一阶谓词形式表示。 (1) 雪是白的。 (2) 数a和数b之和大于数c。 (3) 201班的学生每人都有一台笔记本电脑。 (4) 如果明天天气晴朗且我们有时间，则我们去郊游。 (5) 一个三角形是等腰三角形，当且仅当其有两个角相等。 2. 什么是推理规则？举例说明一个推理形式可作为推理规则的充分必要条件是什么？ 3. 求下列谓词公式的子句集。 (1) xy(P(x，y)∧Q(x，y)) (2) xy(P(x，y)→Q(x，y)) (3) xy((P(x，y)∨Q(x，y))→R(x，y)) (4) x(P(x)→y(P(y)∧R(x，y))） (5) x(P(x)∧y(P(y)→R(x，y))) 4. 试判断下列子句集中哪些是不可满足的。 (1) S={P(y)∨瘙綈Q(y)，瘙綈P(f(x))∨Q(y)} (2) S={瘙綈P(x)∨Q(x)，瘙綈Q(y)∨R(y)，P(a)，瘙綈R(a)} (3) S={瘙綈P(x)∨瘙綈Q(y)∨瘙綈L(x，y)，P(a)，瘙綈R(z)∨L(a，z)，R(b)，Q(b)} (4) S={P(x)∨Q(x)∨R(x)，瘙綈P(y)∨R(y)，瘙綈Q(a)，瘙綈R(b)} (5) S={P(x)∨Q(x)，瘙綈Q(y)∨R(y)，瘙綈P(z)∨Q(z)，瘙綈R(u)} 5. 对下列各题分别证明，G是否可肯定是F、F1、F2……的逻辑结论。 (1) F： (P∨Q)∧(P→R)∧(Q→S) G： R∨S (2) F1： x(P(x)→y(Q(y)→L(x，y))) F2： x(P(x)∧y(R(y)→L(x，y))) G： x(R(x)→瘙綈Q(x)) (3) F1： x(P(x)→Q(x)∧R(x)) F2： x(P(x)∧S(x)) G： x(S(x)∧R(x)) 6. 设已知： (1) 凡是清洁的东西就有人喜欢； (2) 人们都不喜欢苍蝇。 试用谓词公式表示这两个命题，并用归结原理证明： 苍蝇是不清洁的。 7. 某公司招聘工作人员，有A、B、C三人应聘，经面试后，公司表示如下想法： (1) 三人中至少录取一人； (2) 如果录取A而不录取B，则一定录取C； (3) 如果录取B，则一定录取C。 试用谓词公式表示这三个命题，并用归结原理求证： 公司一定录取C。 8. 张某被盗，公安局派出5个侦查员去调查。研究案情时，侦查员A说“赵与钱中至少有一人作案”； 侦查员B说“钱与孙中至少有一人作案”； 侦查员C说“孙与李中至少有一人作案”； 侦查员D说“赵与孙中至少有一人与此案无关”； 侦查员E说“钱与李中至少有一人与此案无关”。假设这5个侦查员的话都是可信的，用谓词公式表示这5句话，并用归结原理推出谁是盗窃犯。 9. 试画出例528的(线性)归结演绎树。 10. Horn子句逻辑与计算机程序语言有何关系？为什么称PROLOG语言为逻辑程序设计语言？