1、第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 第 5 章 基于谓词逻辑的机器推理 5.1 一阶谓词逻辑一阶谓词逻辑5.2 5.2 归结演绎推理归结演绎推理 5.3 5.3 应用归结原理求取问题答案应用归结原理求取问题答案 5.4 5.4 归结策略归结策略 5.5 5.5 归结反演程序举例归结反演程序举例 5.6 Horn5.6 Horn子句归结与逻辑程序子句归结与逻辑程序 5.7 5.7 非归结演绎推理非归结演绎推理 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 5.1 一阶谓词逻辑一阶谓词逻辑 5.1.1 5.1.1 谓词、函数、量词谓词、函数、量词 设a1,
2、a2,an表示个体对象,A表示它们的属性、状态或关系,则表达式 A(a1,a2,an)在谓词逻辑中就表示一个(原子)命题。例如,(1)素数(2),就表示命题“2是个素数”。(2)好朋友(张三,李四),就表示命题“张三和李四是好朋友”。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 P(x1,x2,xn)一般地,表达式 在谓词逻辑中称为n元谓词。其中P是谓词符号，也称谓词，代表一个确定的特征或关系(名)。x1,x2,xn称为谓词的参量或者项，一般表示个体。个体变元的变化范围称为个体域（或论述域），包揽一切事物的集合称为全总个体域。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的
3、机器推理 为了表达个体之间的对应关系，我们引入通常数学中函数的概念和记法。例如我们用father(x)表示x的父亲，用sum(x,y)表示数x和y之和，一般地，我们用如下形式：f(x1,x2,xn)表示个体变元x1,x2,xn所对应的个体y，并称之为n元个体函数，简称函数（或函词、函词命名式）。其中f是函数符号，有了函数的概念和记法，谓词的表达能力就更强了。例如，我们用Doctor(father(Li)表示“小李的父亲是医生”，用E(sq(x),y)表示“x的平方等于y”。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 以后我们约定用大写英文字母作为谓词符号,用小写字母f,g,h
4、等表示函数符号,用小写字母x,y,z等作为个体变元符号,用小写字母a,b,c等作为个体常元符号。我们把“所有”、“一切”、“任一”、“全体”、“凡是”等词统称为全称量词,记为 x;把“存在”、“有些”、“至少有一个”、“有的”等词统称为存在量词,记为x。)()(xNxMx其中M(x)表示“x是人”,N(x)表示“x有名字”,该式可读作“对于任意的x,如果x是人,则x有名字”。这里的个体域取为全总个体域。如果把个体域取为人类集合,则该命题就可以表示为)(xxN第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 同理,我们可以把命题“存在不是偶数的整数”表示为)()(xExGx其中G(x
5、)表示“x是整数”,E(x)表示“x是偶数”。此式可读作“存在x,x是整数并且x不是偶数”。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 不同的个体变元,可能有不同的个体域。为了方便和统一起见,我们用谓词表示命题时,一般总取全总个体域,然后再采取使用限定谓词的办法来指出每个个体变元的个体域。具体来讲,有下面两条：(1)对全称量词,把限定谓词作为蕴含式之前件加入,即 x(P(x)。(2)对存在量词,把限定量词作为一个合取项加入,即 x(P(x)。这里的P(x)就是限定谓词。我们再举几个例子。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例 5.1不存在最大的整数
6、,我们可以把它翻译为),()()(yxDyGyxGx或),()()(xyDyGyxGx例例 5.2对于所有的自然数,均有x+yx),()()(xyxSyNxNyx例例 5.3某些人对某些食物过敏),()()(yxGyFxMyx第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 5.1.2 谓词公式谓词公式定义定义1 (1)个体常元和个体变元都是项。(2)设f是n元函数符号,若t1,t2,tn是项,则f(t1,t2,tn)是项。(3)只有有限次使用(1),(2)得到的符号串才是项。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义2 设P为n元谓词符号，t1,t2,
7、tn为项，则P(t1,t2,tn)称为原子谓词公式，简称原子公式或者原子。从原子谓词公式出发，通过命题联结词和量词，可以组成复合谓词公式。下面我们给出谓词公式的严格定义，即谓词公式的生成规则。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义3 (1)原子公式是谓词公式。(2)若A,B是谓词公式，则A,AB,AB,AB,A B,xA,xA也是谓词公式。(3)只有有限步应用(1)，(2)生成的公式才是谓词公式。由项的定义，当t1,t2,tn全为个体常元时，所得的原子谓词公式就是原子命题公式（命题符号）。所以，全体命题公式也都是谓词公式。谓词公式亦称为谓词逻辑中的合适（式）合适
8、（式）公式公式，记为Wff。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 紧接于量词之后被量词作用(即说明)的谓词公式称为该量词的辖域。例如：(1)xP(x)。(2)x(H(x)G(x,y)。(3)xA(x)B(x)。其中(1)中的P(x)为x的辖域,(2)中的H(x)G(x,y)为x的辖域,(3)中的A(x)为x的辖域,但B(x)并非x的辖域。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 量词后的变元如 x,y中的x,y称为量词的指导变元(或作用变元),而在一个量词的辖域中与该量词的指导变元相同的变元称为约束变元,其他变元(如果有的话)称为自由变元,例如(2)
9、中的x为约束变元,而y为自由变元,(3)中A(x)中的x为约束变元,但B(x)中的x为自由变元。例如(3),一个变元在一个公式中既可约束出现,又可自由出现,但为了避免混淆,通常通过改名规则,使得一个公式中一个变元仅以一种形式出现。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 约束变元的改名规则如下：(1)对需改名的变元,应同时更改该变元在量词及其辖域中的所有出现。(2)新变元符号必须是量词辖域内原先没有的,最好是公式中也未出现过的。例如公式 xP(x)Q(x)可改为 yP(y)Q(x),但两者的意义相同。在谓词前加上量词,称作谓词中相应的个体变元被量化,例如xA(x)中的x被量
10、化,yB(y)中y被量化。如果一个谓词中的所有个体变元都被量化,则这个谓词就变为一个命题。例如,设P(x)表示“x是素数”,则 xP(x),xP(x)就都是命题。这样我们就有两种从谓词(即命题函数)得到命题的方法：一种是给谓词中的个体变元代入个体常元,另一种就是把谓词中的个体变元全部量化。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 把上面关于量化的概念也可以推广到谓词公式。于是，我们便可以说，如果一个公式中的所有个体变元都被量化，或者所有变元都是约束变元（或无自由变元），则这个公式就是一个命题。特别地，我们称 xA(x)为全称命题，xA(x)为特称命题。对于这两种命题，当个体
11、域为有限集时（设有n个元素），有下面的等价式：xA(x)A(a1)A(a2)A(an)xA(x)A(a1)A(a2)A(an)这两个式子也可以推广到个体域为可数无限集。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义4 设A为如下形式的谓词公式：B1B2Bn 其中Bi(i=1,2,n)形如L1L2Lm，Lj(j=1,2,m)为原子公式或其否定，则A称为合取范式。例如：(P(x)Q(y)(乛P(x)Q(y)R(x,y)(乛Q(y)乛R(x,y)就是一个合取范式。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义5 设A为如下形式的命题公式：B1B2Bn
12、其中Bi(i=1,2,n)形如L1L2Lm，Lj(j=1,2,m)为原子公式或其否定，则A称为析取范式。例如：(P(x)乛Q(y)R(x,y)(乛P(x)Q(y)(乛P(x)R(x,y)就是一个析取范式。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义6 设P为谓词公式，D为其个体域，对于D中的任一解释I：(1)若P恒为真，则称P在D上永真（或有效）或是D上的永真式。(2)若P恒为假，则称P在D上永假（或不可满足）或是D上的永假式。(3)若至少有一个解释,可使P为真，则称P在D上可满足或是D上的可满足式。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定
13、义7 设P为谓词公式，对于任何个体域：(1)若P都永真，则称P为永真式。(2)若P都永假，则称P为永假式。(3)若P都可满足，则称P为可满足式。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 5.1.3 谓词逻辑中的形式演绎推理谓词逻辑中的形式演绎推理 由上节所述，我们看到，利用谓词公式可以将自然语言中的陈述语句表示为一种形式化的符号表达式。那么，利用谓词公式，我们同样可以将形式逻辑中抽象出来的推理规则形式化为一些符号变换公式。表3.1和表3.2就是形式逻辑中常用的一些逻辑等价式和逻辑蕴含式，即推理规则的符号表示形式。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理
14、表表5.1 常用逻辑等价式常用逻辑等价式 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 表5.2 常用逻辑蕴含式 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例5.4 设有前提：(1)凡是大学生都学过计算机；(2)小王是大学生。试问：小王学过计算机吗？解 令S(x)：x是大学生;M(x)：x学过计算机;a：小王。则
15、上面的两个命题可用谓词公式表示为 (1)x(S(x)M(x)(2)S(a)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 下面我们进行形式推理：(2)x(S(x)M(x)前提 (2)S(a)M(a)(1),US (3)S(a)前提 (4)M(a)(2),(3),I3 得结果：M(a)，即“小王学过计算机”。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例5.5 证明乛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,
16、b)(2),US (4)乛W(a,b)前提 (5)乛P(a,b)(3),(4),I4第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例5.6 证 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)(3),US(6)R(y)乛P(y)(3),(5),I6(7)x(R(x)乛P(x)(6),UG 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 5.2.1 子句集子句集 定义定义1 原子谓词公式及
17、其否定称为文字，若干个文字的一个析取式称为一个子句，由r个文字组成的子句叫r文字子句，1文字子句叫单元子句，不含任何文字的子句称为空子句，记为或NIL。例如下面的析取式都是子句 PQ乛R P(x,y)乛Q(x)5.2 归结演绎推理归结演绎推理第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义2 对一个谓词公式G，通过以下步骤所得的子句集合S，称为G的子句集。(1)消去蕴含词和等值词。可使用逻辑等价式:ABAB A B(乛AB)(乛BA)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 (2)缩小否定词的作用范围，直到其仅作用于原子公式。可使用逻辑等价式:乛(乛A
18、)A 乛(AB)乛A乛B 乛(AB)乛A乛B乛 xP(x)x乛P(x)乛 xP(x)x乛P(x)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 (3)适当改名，使量词间不含同名指导变元和约束变元。(4)消去存在量词。消去存在量词时，同时还要进行变元替换。变元替换分两种情况：若该存在量词在某些全称量词的辖域内，则用这些全称量词指导变元的一个函数代替该存在量词辖域中的相应约束变元，这样的函数称为Skolem函数；若该存在量词不在任何全称量词的辖域内，则用一个常量符号代替该存在量词辖域中的相应约束变元，这样的常量符号称为Skolem常量。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻
19、辑的机器推理 (5)消去所有全称量词。(6)化公式为合取范式。可使用逻辑等价式:A(BC)(AB)(AC)(AB)C (AC)(BC)(7)适当改名，使子句间无同名变元。(8)消去合取词，以子句为元素组成一个集合S。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例5.7 求下面谓词公式的子句集 x yP(x,y)yQ(x,y)R(x,y)解解由步(1)得 x乛yP(x,y)乛 yQ(x,y)R(x,y)由步(2)得 x yP(x,y)yQ(x,y)乛R(x,y)由步(3)得 x yP(x,y)zQ(x,z)乛R(x,z)由步(4)得 x乛P(x,f(x)Q(x,g(x)乛R(
20、x,g(x)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 由步(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)为原谓词公式的子句集。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 需说明的是，在上述求子句集的过程中，当消去存在量词后，把所有
21、全称量词都依次移到整个式子的最左边（或者先把所有量词都依次移到整个式子的最左边，再消去存在量词），再将右部的式子化为合取范式，这时所得的式子称为原公式的称为Skolem标准型。例如，上例中谓词公式的Skolem标准型就是 x乛P(x,f(x)Q(x,g(x)乛P(y,f(y)乛R(y,g(y)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例5.8 设G=xyzuvw(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的子句集
22、为 P(a,x,y),乛Q(f(u,v),w,g(u,v,w)由此例还可看出，一个公式的子句集也可以通过先求前束范式，再求Skolem标准型而得到。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 ()()(0)(1)0,1,0GxP xGP aa PPDFT 它的Skolem标准型是我们给出如下的一个解释I：需说明的是，引入Skolem函数，是由于存在量词在全称量词的辖域之内，其约束变元的取值则完全依赖于全称量词的取值。Skolem函数就反映了这种依赖关系。但注意，Skolem标准型与原公式一般并不等价，例如有公式：则在I下,G=T,而G=F。第第5 5章章 基于谓词逻辑的机器推
23、理基于谓词逻辑的机器推理 定理定理1 把证明一个公式G的不可满足性，转化为证明其子句集S的不可满足性。定义定义3 子句集S是不可满足的，当且仅当其全部子句的合取式是不可满足的。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 5.2.2 命题逻辑中的归结原理命题逻辑中的归结原理 归结演绎推理是基于一种称为归结原理(亦称消解原理principleofresolution)的推理规则的推理方法。归结原理是由鲁滨逊(J.A.Robinson)于1965年首先提出。它是谓词逻辑中一个相当有效的机械化推理方法。归结原理的出现，被认为是自动推理，特别是定理机器证明领域的重大突破。第第5 5章章
24、 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义4 设L为一个文字，则称L与L为互补文字。定义定义5 设C1,C2是命题逻辑中的两个子句，C1中有文字L1，C2中有文字L2，且L1与L2互补，从C1,C2中分别删除L1,L2，再将剩余部分析取起来，记构成的新子句为C12，则称C12为C1,C2的归结式(或消解式)，C1,C2称为其归结式的亲本子句，L1,L2称为消解基。例例3.9 设C1=乛PQR,C2=乛QS,于是C1,C2的归结式为乛PRS 定理2 归结式是其亲本子句的逻辑结果。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 证明 设C1=LC1,C2=乛LC2,C1
25、,C2都是文字的析取式，则C1,C2的归结式为C1C2，因为 C1=C1L=乛(C1L),C2=LC2=(LC2)所以 C1C2=(乛C1L)(LC2)乛(C1C2)=C1C2 证毕。由定理2即得推理规则：C1C2 (C1-L1)(C2-L2)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例3.10 用归结原理验证分离规则：A(AB)B和拒取式(AB)乛B 乛A。解 A(AB)A(乛AB)B (AB)乛B (乛AB)(乛B)乛A 类似地可以验证其他推理规则也都可以经消解原理推出。这就是说，用消解原理就可以代替其他所有的推理规则。再加上这个方法的推理步骤比较机械，这就为机器推理
26、提供了方便。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 推论 设C1,C2是子句集S的两个子句，C12是它们的归结式，则 (1)若用C12代替C1,C2，得到新子句集S1，则由S1的不可满足可推出原子句集S的不可满足。即 S1不可满足 S不可满足 (2)若把C12加入到S中，得到新子句集S2，则S2与原S的同不可满足。即 S2不可满足 S不可满足第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例5.11 证明子句集PQ,P,Q是不可满足的。证证(1)P乛Q(2)乛P(3)Q(4)乛Q 由(1),(2)(5)由(3),(4)第第5 5章章 基于谓词逻辑的机器推理
27、基于谓词逻辑的机器推理 例例5.12 用归结原理证明R是P,(PQ)R,(SU)Q,U的逻辑结果。证 我们先把诸前提条件化为子句形式，再把结论的非也化为子句，由所有子句得到子句集S=P,乛P乛QR,乛SQ,乛UQ,U,乛R，然后对该子句集施行归结，归结过程用下面的归结演绎树表示（见图31）。由于最后推出了空子句，所以子句集S不可满足，即命题公式 P(乛P乛QR)(乛SQ)(乛UQ)U乛R 不可满足，从而R是题设前提的逻辑结果。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 图51 例5.12归结演绎树 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 5.2.3 替换
28、与合一替换与合一 在一阶谓词逻辑中应用消解原理，不像命题逻辑中那样简单，因为谓词逻辑中的子句含有个体变元，这就使寻找含互否文字的子句对的操作变得复杂。例如：C1=P(x)Q(x)C2=P(a)R(y)直接比较，似乎两者中不含互否文字，但如果我们用a替换C1中的x，则得到 C1=P(a)Q(a)C2=P(a)R(y)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 于是根据命题逻辑中的消解原理，得C1和C2的消解式 C3=Q(a)R(y)所以，要在谓词逻辑中应用消解原理，则一般需要对个体变元作适当的替换。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义6 一个替
29、换(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都是不含变元的项（称为基项）时，该替换称为基替换；没有元素的替换称为空替换，记作，它表示不作替换。例如：第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 a/x,g(y)/y,f(g(b)/z就是一个替换，而g(y)/x,f(x)/y则不是一个替换,因为x与y出现了循环替换。下面我们将项、原子公
30、式、文字、子句等统称为表达式，没有变元的表达式称为基表达式，出现在表达式E中的表达式称为E的子表达式。定义定义7 设=t1/x1,tn/xn是一个替换，E是一个表达式，把对E施行替换，即把E中出现的个体变元xj(1jn)都用tj替换，记为E，所得的结果称为E在下的例(instance)。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义8 设=t1/x1,tn/xn,=u1/y1,um/ym是两个替换，则将集合 t1/x1,tn/xn,u1/y1,um/ym 中凡符合下列条件的元素删除：(1)ti/xi 当ti=xi (2)ui/yi当yix1,xn 如此得到的集合仍然是一
31、个替换，该替换称为与的复合或乘积，记为。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例5.13 设=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 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义9 设S=F1,F2,Fn是一个原子谓词公式集，若存在一个替换，可使F1=F2=Fn，则称为S的一个合一(Unifier)，称S为可合一的。一个公式集的合一一般不唯一。定义10
32、设是原子公式集S的一个合一，如果对S的任何一个合一，都存在一个替换，使得 =则称为S的最一般合一(MostGeneralUnifier)，简称MGU。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例5.14 设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 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 可以看出，如果能找到一个公式集的合一，特别是最一般合一，则可使互否的文字的形式结构完全一致起来
33、，进而达到消解的目的。如何求一个公式集的最一般合一？有一个算法，可以求任何可合一公式集的最一般合一。为了介绍这个算法，我们先引入差异集的概念。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义定义11 设S是一个非空的具有相同谓词名的原子公式集，从S中各公式的左边第一个项开始，同时向右比较，直到发现第一个不都相同的项为止，用这些项的差异部分组成一个集合，这个集合就是原公式集S的一个差异集。例例3.15 设S=P(x,y,z),P(x,f(a),h(b)，则不难看出，S有两个差异集 D1=y,f(a)D2=z,h(b)设S为一非空有限具有相同谓词名的原子谓词公式集，下面给出求其最
34、一般合一的算法。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 合一算法合一算法(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=ktk/xk，k=k+1，然后转步2;步步5 算法停止，S的最一般合一不存在。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例3.16 求公式集S=P(a,x,f(g(y),P(z,
35、h(z,u),f(u)的最一般合一。解解 k=0：S0=S,0=,S0不是单元素集，求得D0=a,z，其中z是变元，且不在a中出现，所以有 1=0a/z=a/z=a/zS1=S0a/z=P(a,x,f(g(y),P(a,h(a,u),f(u)k=1:S1不是单元素集，求得D1=x,h(a,u)，第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 所以2=1h(a,u)/x=a/zh(a,u)/x=a/u,h(a,u)/xS2=S1h(a,u)/x=P(a,h(a,u),f(g(y),P(a,h(a,u),f(u)k=2:S2不是单元素集，D2=g(y),u，3=2g(y)/u=a/z
36、,h(a,g(y)/x,g(y)/uS3=S2g(y)/u=P(a,h(a,g(y),f(g(y),P(a,h(a,g(y),f(g(y)=P(a,h(a,g(y),f(g(y)k=3:S3已是单元素集，所以3就是S的最一般合一。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例3.17 判定S=P(x,x),P(y,f(y)是否可合一？解解k=0:S0=S,0=,S0不是单元素集，D0=x,y1=0y/x=y/xS1=S0y/x=P(y,y),P(y,f(y)k=1:第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 S1不是单元素集，D1=y,f(y)，由于变元y
37、在项f(y)中出现，所以算法停止，S不存在最一般合一。从合一算法可以看出，一个公式集S的最一般合一可能是不唯一的，因为如果差异集Dk=ak,bk，且ak和bk都是个体变元，则下面两种选择都是合适的：k+1=kbk/ak或k+1=kak/bk第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定理定理3（合一定理）如果S是一个非空有限可合一的公式集，则合一算法总是在步2停止，且最后的k即是S的最一般合一。本定理说明任一非空有限可合一的公式集，一定存在最一般合一，而且用合一算法总能找到最一般合一，这个最一般合一也就是当算法终止在步2时，最后的合一k。第第5 5章章 基于谓词逻辑的机器推理
38、基于谓词逻辑的机器推理 3.2.4 谓词逻辑中的归结原理谓词逻辑中的归结原理 定义定义12 设C1,C2是两个无相同变元的子句，L1,L2分别是C1,C2中的两个文字，如果L1和L2有最一般合一，则子句(C1-L1)(C2-L2)称作C1和C2的二元归结式(二元消解式)，C1和C2称作归结式的亲本子句，L1和L2称作消解文字。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例3.18 设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
39、(a)-P(a)(P(a),R(y)-P(a)=Q(a),R(y)=Q(a)R(y)所以，Q(a)R(y)是C1和C2的二元归结式。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例3.19 设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)第第5 5章章
40、基于谓词逻辑的机器推理基于谓词逻辑的机器推理 可见,在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的归结式 (f(a)R(b)定义定义13 如果子句C中，两个或两个以上的文字有一个最一般合一，则C称为C的因子，如果C是单元子句，则C称为C的单因子。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例3.20 设C=P(x)P(f(y)乛Q(x),令=f(y)/x，于是C=P(f(y)乛Q(f(y)是C的因子。定义定义14
41、 子句C1,C2的消解式，是下列二元消解式 之一：(1)C1和C2的二元消解式;(2)C1和C2的因子的二元消解式;(3)C1的因子和C2的二元消解式;(4)C1的因子和C2的因子的二元消解式。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定理定理4 谓词逻辑中的消解式是它的亲本子句的逻辑结果。(证明类似于定理2，故从略。)由此定理我们即得谓词逻辑中的推理规则：C1C2 (C1-L1)(C2-L2)其中C1,C2是两个无相同变元的子句，L1,L2分别是C1,C2中的文字，为L1与L2的最一般合一。此规则称为谓词逻辑中的消解原理（或归结原理）。第第5 5章章 基于谓词逻辑的机器推
42、理基于谓词逻辑的机器推理 例例3.21 求证G是A1和A2的逻辑结果。A1:x(P(x)(Q(x)R(x)A2:x(P(x)S(x)G:x(S(x)R(x)证证 我们用反证法，即证明A1A2乛G不可满足。首先求得子句集S：第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 (1)乛P(x)Q(x)(2)乛P(y)R(y)(3)P(a)(4)S(a)(5)乛S(z)乛R(z)(乛G)然后应用消解原理，得(6)R(a)(2),(3),1=a/y(7)乛R(a)(4),(5),2=a/z(8)(6),(7)所以S是不可满足的，从而G是A1和A2的逻辑结果。(A1)(A2)S第第5 5章章
43、基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例3.22 设已知：(1)能阅读者是识字的；(2)海豚不识字；(3)有些海豚是很聪明的。试证明：有些聪明者并不能阅读。证 首先，定义如下谓词：R(x)：x能阅读。L(x)：x识字。I(x)：x是聪明的。D(x)：x是海豚。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 然后把上述各语句翻译为谓词公式：(1)x(R(x)L(x)(2)x(D(x)乛L(x)已知条件(3)x(D(x)I(x)(4)x(I(x)乛R(x)需证结论 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 求题设与结论否定的子句集，得(1)乛R(x)L(
44、x)(2)乛D(y)乛L(y)(3)D(a)(4)I(a)(5)乛I(z)R(z)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 归结得(6)R(a)(5)，(4)，a/z(7)L(a)(6)，(1)，a/x(8)乛D(a)(7),(2),a/y(9)(8),(3)这个归结过程的演绎树如图32所示。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 由以上例子可以看出，谓词逻辑中的消解原理也可以代替其他推理规则。上面我们通过推导空子句，证明了子句集的不可满足性，于是存在问题：对于任一不可满足的子句集，是否都能通过归结原理推出空子句呢？回答是肯定的。定理定理5（归结原理的
45、完备性定理）如果子句集S是不可满足的，那么必存在一个由S推出空子句的消解序列。(该定理的证明要用到Herbrand定理，故从略。)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 图5-2 例3.22 归结演绎树 第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 归结原理除了能用于对已知结果的证明外，还能用于对未知结果的求解，即能求出问题的答案来。请看下例。例例3.23 已知:(1)如果x和y是同班同学，则x的老师也是y的老师。(2)王先生是小李的老师。(3)小李和小张是同班同学。问：小张的老师是谁？5.3 应用归结原理求取问题答案应用归结原理求取问题答案第第5 5章章
46、 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 解解 设谓词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:x T(x,Zhang)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 于是，求F1F2F3 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
47、,y)T(Wang,y)由(1),(2),Wang/z,Li/x(6)C(Li,Zhang)由(4),(5),Wang/u,Zhang/y(7)由(3),(6)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 这说明，小张的老师确实是存在的。那么，为了找到这位老师，我们给原来的求证谓词的子句再增加一个谓词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)第第5 5章章 基
48、于谓词逻辑的机器推理基于谓词逻辑的机器推理 可以看出，归结到这一步，求证的目标谓词已被消去，即求证已成功，但还留下了谓词ANS(Wang)。由于该谓词中原先的变元与目标谓词T(u,Zhang)中的一致，所以，其中的Wang也就是变元u的值。这样，我们就求得了小张的老师也是王老师。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 上例虽然是一个很简单的问题，但它给了我们一个利用归结原理求取问题答案的方法，那就是：先为待求解的问题找一个合适的求证目标谓词；再给增配（以析取形式）一个辅助谓词，且该辅助谓词中的变元必须与对应目标谓词中的变元完全一致；然后进行归结，当某一步的归结式刚好只剩下
49、辅助谓词时，辅助谓词中原变元位置上的项（一般是常量）就是所求的问题答案。需说明的是，辅助谓词（如此题中的ANS）是一个形式谓词，其作用仅是提取问题的答案，因而也可取其他谓词名。有些文献中就用需求证的目标谓词。如对上例，就取T(u,Zhang)为辅助谓词。第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例例3.24 设有如下关系:(1)如果x是y的父亲，y又是z的父亲，则x是z的祖父。(2)老李是大李的父亲。(3)大李是小李的父亲。问：上述人员中谁和谁是祖孙关系？解 先把上述前提中的三个命题符号化为谓词公式：F1:x y z(F(x,y)F(y,z)G(x,z)F2:F(Lao,D
50、a)F3:F(Da,Xiao)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 并求其子句集如下:(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的祖父)第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 把其否定化为子句形式再析取一个辅助谓词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)G
