人工智能课件3之基于谓词逻辑的机器

第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.1 一阶谓词逻辑一阶谓词逻辑3.2 归结演绎推理归结演绎推理3.3 应用归结原理求取问题答案应用归结原理求取问题答案3.4 归结策略归结策略3.5 非归结演绎推理非归结演绎推理第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.1 一阶谓词逻辑一阶谓词逻辑 3.1.1谓词、函数、量词设a1,a2,an表示个体对象，A表示它们的属性、状态或关系，则表达式A(a1,a2,an)在谓词逻辑中就表示一个(原子)命题。例如，1.素数(2)，就表示命题“2是个素数”。2.好朋友(张三，李四)，就表示命题“张三和李四是好朋友”。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 表达式P(x1,x2,xn)称为n元谓词。其中P是谓词符号，也称谓词，代表一个确定的特征或关系(名)。x1,x2,xn称为谓词的参量或者项，一般表示个体。个体变元的变化范围称为个体域（或论述域），包揽一切事物的集合称为全总个体域。为了表达个体之间的对应关系，我们引入通常数学中函数的概念和记法。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例如我们用father(x)表示x的父亲，用sum(x,y)表示数x和y之和，一般地，我们用如下形式：f(x1,x2,xn)表示个体变元x1,x2,xn所对应的个体y，并称之为n元个体函数，简称函数（或函词、函词命名式）。其中f是函数符号，有了函数的概念和记法，谓词的表达能力就更强了。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例如，我们用Doctor(father(Li)表示“小李的父亲是医生”，用E(sq(x),y)表示“x的平方等于y”。以后我们约定用大写英文字母作为谓词符号，用小写字母f,g,h等表示函数符号，用小写字母x,y,z等作为个体变元符号，用小写字母a,b,c等作为个体常元符号。我们把“所有”、“一切”、“任一”、“全体”、“凡是”等词统称为全称量词，记为x;把“存在”、“有些”、“至少有一个”、“有的”等词统称为存在量词，记为x。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 引入量词后，谓词的表达能力就大大扩充了，例如命题“凡是人都有名字”，就可以表示为x(M(x)N(x)其中M(x)表示“x是人”，N(x)表示“x有名字”，该式可读作“对于任意的x，如果x是人，则x有名字”。这里的个体域取为全总个体域。如果把个体域取为人类集合，则该命题就可以表示为第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 xN(x)同理，我们可以把命题“存在不是偶数的整数”表示为x(G(x)乛E(x)其中G(x)表示“x是整数”，E(x)表示“x是偶数”。此式可读作“存在x，x是整数并且x不是偶数”。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 不同的个体变元，可能有不同的个体域。为了方便和统一起见，我们用谓词表示命题时，一般总取全总个体域，然后再采取使用限定谓词的办法来指出每个个体变元的个体域。具体来讲，有下面两条：(1)对全称量词，把限定谓词作为蕴含式之前件加入，即x(P(x)。(2)对存在量词，把限定量词作为一个合取项加入，即x(P(x)。这里的P(x)就是限定谓词。我们再举几个例子。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例3.1不存在最大的整数，我们可以把它翻译为乛x(G(x)y(G(y)D(x,y)或x(G(x)y(G(y)D(y,x)例3.2对于所有的自然数，均有x+yxxy(N(x)N(y)S(x,y,x)例3.3某些人对某些食物过敏xy(M(x)F(y)G(x,y)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.1.2谓词公式由上节可以看出，用谓词、量词及真值联结词可以表达相当复杂的命题。抽象地来看，我们把命题的这种符号表达式称为谓词公式，下面我们给出谓词公式的定义。定义1(1)个体常元和个体变元都是项。(2)设f是n元函数符号，若t1,t2,tn是项，则f(t1,t2,tn)是项。(3)只有有限次使用(1)，(2)得到的符号串才是项。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义2设P为n元谓词符号，t1,t2,tn为项，则P(t1,t2,tn)称为原子谓词公式，简称原子公式或者原子。从原子谓词公式出发，通过命题联结词和量词，可以组成复合谓词公式。下面我们给出谓词公式的严格定义，即谓词公式的生成规则。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义3(1)原子公式是谓词公式。(2)若A,B是谓词公式，则A,AB,AB,AB,AB,xA,xA也是谓词公式。(3)只有有限步应用(1)，(2)生成的公式才是谓词公式。由项的定义，当t1,t2,tn全为个体常元时，所得的原子谓词公式就是原子命题公式（命题符号）。所以，全体命题公式也都是谓词公式。谓词公式亦称为谓词逻辑中的合适（式）公式，记为Wff。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 紧接于量词之后被量词作用（即说明）的谓词公式称为该量词的辖域。例如：(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的辖域。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 量词后的变元如x,y中的x,y称为量词的指导变元（或作用变元），而在一个量词的辖域中与该量词的指导变元相同的变元称为约束变元，其他变元（如果有的话）称为自由变元，例如(2)中的x为约束变元，而y为自由变元，(3)中A(x)中的x为约束变元，但B(x)中的x为自由变元。例如(3)，一个变元在一个公式中既可约束出现，又可自由出现，但为了避免混淆，通常通过改名规则，使得一个公式中一个变元仅以一种形式出现。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 约束变元的改名规则如下：(1)对需改名的变元，应同时更改该变元在量词及其辖域中的所有出现。(2)新变元符号必须是量词辖域内原先没有的，最好是公式中也未出现过的。例如公式xP(x)Q(x)可改为yP(y)Q(x),但两者的意义相同。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 需要说明的是，仅个体变元被量化的谓词称为一阶谓词。如果不仅个体变元被量化，而且函数符号和谓词符号也被量化，则那样的谓词称为二阶谓词。例如，pxP(x)就是一个二阶谓词。本书只涉及一阶谓词，所以，以后提及的谓词都是指一阶谓词。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 把上面关于量化的概念也可以推广到谓词公式。于是，我们便可以说，如果一个公式中的所有个体变元都被量化，或者所有变元都是约束变元（或无自由变元），则这个公式就是一个命题。特别地，我们称xA(x)为全称命题，xA(x)为特称命题。对于这两种命题，当个体域为有限集时（设有n个元素），有下面的等价式：xA(x)A(a1)A(a2)A(an)xA(x)A(a1)A(a2)A(an)这两个式子也可以推广到个体域为可数无限集。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义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)就是一个合取范式。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义5设A为如下形式的命题公式：B1B2Bn其中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)就是一个析取范式。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义6设P为谓词公式，D为其个体域，对于D中的任一解释I：(1)若P恒为真，则称P在D上永真（或有效）或是D上的永真式。(2)若P恒为假，则称P在D上永假（或不可满足）或是D上的永假式。(3)若至少有一个解释,可使P为真，则称P在D上可满足或是D上的可满足式。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义7设P为谓词公式，对于任何个体域：(1)若P都永真，则称P为永真式。(2)若P都永假，则称P为永假式。(3)若P都可满足，则称P为可满足式。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.1.3谓词逻辑中的形式演绎推理由上节所述，我们看到，利用谓词公式可以将自然语言中的陈述语句表示为一种形式化的符号表达式。那么，利用谓词公式，我们同样可以将形式逻辑中抽象出来的推理规则形式化为一些符号变换公式。表3.1和表3.2就是形式逻辑中常用的一些逻辑等价式和逻辑蕴含式，即推理规则的符号表示形式。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 表3.1常用逻辑等价式第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 表3.2常用逻辑蕴含式第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例3.4设有前提：(1)凡是大学生都学过计算机；(2)小王是大学生。试问：小王学过计算机吗？解令S(x)：x是大学生;M(x)：x学过计算机;a：小王。则上面的两个命题可用谓词公式表示为(1)x(S(x)M(x)(2)S(a)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 下面我们进行形式推理：(2)x(S(x)M(x)前提(2)S(a)M(a)(1),US(3)S(a)前提(4)M(a)(2),(3),I3得结果：M(a)，即“小王学过计算机”。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.2 归结演绎推理归结演绎推理3.2.1子句集定义1原子谓词公式及其否定称为文字，若干个文字的一个析取式称为一个子句，由r个文字组成的子句叫r文字子句，1文字子句叫单元子句，不含任何文字的子句称为空子句，记为或NIL。例如下面的析取式都是子句PQ乛RP(x,y)乛Q(x)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义2对一个谓词公式G，通过以下步骤所得的子句集合S，称为G的子句集。(1)消去蕴含词和等值词。可使用逻辑等价式:AB乛ABAB(乛AB)(乛BA)(2)缩小否定词的作用范围，直到其仅作用于原子公式。可使用逻辑等价式:乛(乛A)A乛(AB)乛A乛B第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 乛(AB)乛A乛B乛xP(x)x乛P(x)乛xP(x)x乛P(x)(3)适当改名，使量词间不含同名指导变元和约束变元。(4)消去存在量词。消去存在量词时，同时还要进行变元替换。变元替换分两种情况：若该存在量词在某些全称量词的辖域内，则用这些全称量词指导变元的一个函数代替该存在量词辖域中的相应约束变元，这样的函数称为Skolem函数；第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 若该存在量词不在任何全称量词的辖域内，则用一个常量符号代替该存在量词辖域中的相应约束变元，这样的常量符号称为Skolem常量。(5)消去所有全称量词。(6)化公式为合取范式。可使用逻辑等价式:A(BC)(AB)(AC)(AB)C(AC)(BC)(7)适当改名，使子句间无同名变元。(8)消去合取词，以子句为元素组成一个集合S。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例3.7求下面谓词公式的子句集xyP(x,y)yQ(x,y)R(x,y)解解由步(1)得x乛yP(x,y)乛yQ(x,y)R(x,y)由步(2)得xyP(x,y)yQ(x,y)乛R(x,y)由步(3)得xyP(x,y)zQ(x,z)乛R(x,z)由步(4)得x乛P(x,f(x)Q(x,g(x)乛R(x,g(x)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 由步(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)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 为原谓词公式的子句集。需说明的是，在上述求子句集的过程中，当消去存在量词后，把所有全称量词都依次移到整个式子的最左边（或者先把所有量词都依次移到整个式子的最左边，再消去存在量词），再将右部的式子化为合取范式，这时所得的式子称为原公式的称为Skolem标准型。例如，上例中谓词公式的Skolem标准型就是x乛P(x,f(x)Q(x,g(x)乛P(y,f(y)乛R(y,g(y)一个公式的子句集也可以通过先求前束范式，再求Skolem标准型而得到。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定定理理1把证明一个公式G的不可满足性，转化为证明其子句集S的不可满足性。定定义义3子句集S是不可满足的，当且仅当其全部子句的合取式是不可满足的。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.2.2命题逻辑中的归结原理归结演绎推理是基于一种称为归结原理(亦称消解原理principleofresolution)的推理规则的推理方法。归结原理是由鲁滨逊(J.A.Robinson)于1965年首先提出。它是谓词逻辑中一个相当有效的机械化推理方法。归结原理的出现，被认为是自动推理，特别是定理机器证明领域的重大突破。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 定义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第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 图31例3.12归结演绎树第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.2.3替换与合一在一阶谓词逻辑中应用消解原理，不像命题逻辑中那样简单，因为谓词逻辑中的子句含有个体变元，这就使寻找含互否文字的子句对的操作变得复杂。例如：C1=P(x)Q(x)C2=P(a)R(y)直接比较，似乎两者中不含互否文字，但如果我们用a替换C1中的x，则得到C1=P(a)Q(a)C2=P(a)R(y)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 于是根据命题逻辑中的消解原理，得C1和C2的消解式C3=Q(a)R(y)所以，要在谓词逻辑中应用消解原理，则一般需要对个体变元作适当的替换。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例3.22设已知：(1)能阅读者是识字的；(2)海豚不识字；(3)有些海豚是很聪明的。试证明：有些聪明者并不能阅读。证首先，定义如下谓词：R(x)：x能阅读。L(x)：x识字。I(x)：x是聪明的。D(x)：x是海豚。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 然后把上述各语句翻译为谓词公式：(1)x(R(x)L(x)(2)x(D(x)乛L(x)已知条件(3)x(D(x)I(x)(4)x(I(x)乛R(x)需证结论第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 求题设与结论否定的子句集，得(1)乛R(x)L(x)(2)乛D(y)乛L(y)(3)D(a)(4)I(a)(5)乛I(z)R(z)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 归结得(6)R(a)(5)，(4)，a/z(7)L(a)(6)，(1)，a/x(8)乛D(a)(7),(2),a/y(9)(8),(3)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 上面我们通过推导空子句，证明了子句集的不可满足性，于是存在问题：对于任一不可满足的子句集，是否都能通过归结原理推出空子句呢？回答是肯定的。定理5（归结原理的完备性定理）如果子句集S是不可满足的，那么必存在一个由S推出空子句的消解序列。(该定理的证明要用到Herbrand定理，故从略。)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 图3-2例3.22归结演绎树第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.3 应用归结原理求取问题答案应用归结原理求取问题答案 归结原理除了能用于对已知结果的证明外，还能用于对未知结果的求解，即能求出问题的答案来。请看下例。例3.23已知:(1)如果x和y是同班同学，则x的老师也是y的老师。(2)王先生是小李的老师。(3)小李和小张是同班同学。问：小张的老师是谁？第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 解设谓词T(x,y)表示x是y的老师，C(x,y)表示x与y是同班同学，则已知可表示成如下的谓词公式：F1:xyz(C(x,y)T(z,x)T(z,y)F2:T(Wang,Li)F3:C(Li,Zhang)为了得到问题的答案，我们先证明小张的老师是存在的，即证明公式：G:xT(x,Zhang)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 于是，求F1F2F3G的子句集如下:(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)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 这说明，小张的老师确实是存在的。那么，为了找到这位老师，我们给原来的求证谓词的子句再增加一个谓词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)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 可以看出，归结到这一步，求证的目标谓词已被消去，即求证已成功，但还留下了谓词ANS(Wang)。由于该谓词中原先的变元与目标谓词T(u,Zhang)中的一致，所以，其中的Wang也就是变元u的值。这样，我们就求得了小张的老师也是王老师。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 上例虽然是一个很简单的问题，但它给了我们一个利用归结原理求取问题答案的方法，那就是：先为待求解的问题找一个合适的求证目标谓词；再给增配（以析取形式）一个辅助谓词，且该辅助谓词中的变元必须与对应目标谓词中的变元完全一致；然后进行归结，当某一步的归结式刚好只剩下辅助谓词时，辅助谓词中原变元位置上的项（一般是常量）就是所求的问题答案。需说明的是，辅助谓词（如此题中的ANS）是一个形式谓词，其作用仅是提取问题的答案，因而也可取其他谓词名。有些文献中就用需求证的目标谓词。如对上例，就取T(u,Zhang)为辅助谓词。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.4 归结策略归结策略 3.4.1问题的提出前面我们介绍了归结原理及其应用，但前面的归结推理都是用人工实现的。而人们研究归结推理的目的主要是为了更好地实现机器推理，或者说自动推理。那么，现在就存在问题：归结原理如何在机器上实现？把归结原理在机器上实现，就意味着要把归结原理用算法表示，然后编制程序，在计算机上运行。下面我们给出一个实现归结原理的一般性算法：第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 步1将子句集S置入CLAUSES表；步2若空子句NIL在CLAUSES中，则归结成功，结束。步3若CLAUSES表中存在可归结的子句对，则归结之，并将归结式并入CLAUSES表，转步2；步4归结失败，退出。可以看出，这个算法并不复杂，但问题是在其步3中应该以什么样的次序从已给的子句集S出发寻找可归结的子句对而进行归结呢？第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 一种简单而直接的想法就是逐个考察CLAUSES表中的子句，穷举式地进行归结。可采用这样的具体作法：第一轮归结先让CLAUSES表(即原子句集S)中的子句两两见面进行归结，将产生的归结式集合记为S1，再将S1并入CLAUSES得CLAUSESSS1；下一轮归结时，又让新的CLAUSES即SS1与S1中的子句互相见面进行归结，并把产生的归结式集合记为S2，再将S2并入CLAUSES；再一轮归结时，又让SS1S2与S2中的子句进行归结如此进行，直到某一个Sk中出现空子句为止。下面我们举例。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 例3.25设有如下的子句集S，我们用上述的穷举算法归结如下：S:(1)PQ(2)乛PQ(3)P乛Q(4)乛P乛QS1:(5)Q(1),(2)(6)P(1),(3)(7)Q乛Q(1),(4)(8)P乛P(1),(4)(9)Q乛Q(2),(3)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理(10)P乛P(2),(3)(11)乛P(2),(4)(12)乛Q(3),(4)S2:(13)PQ(1),(7)(14)PQ(1),(8)(15)PQ(1),(9)(16)PQ(1),(10)(17)Q(1),(11)(18)P(1),(12)(19)Q(2),(6)(20)乛PQ(2),(7)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理(21)乛PQ(2),(8)(22)乛PQ(2),(9)(23)乛PQ(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)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理(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)第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 可以看出，这个归结方法无任何技巧可言，只是一味地穷举式归结。因而对于如此简单的问题，计算机推导了35步，即产生35个归结式，才导出了空子句。那么，对于一个规模较大的实际问题，其时空开销就可想而知了。事实上，这种方法一般会产生许多无用的子句。这样，随着归结的进行，CLAUSES表将会越来越庞大，以至于机器不能容纳。同时，归结的时间消耗也是一个严重问题。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.4.2几种常用的归结策略1.删除策略在归结过程中可随时删除以下子句：(1)含有纯文字的子句；(2)含有永真式的子句；(3)被子句集中别的子句类含的子句。所谓纯文字，是指那些在子句集中无补的文字。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 删除含有纯文字的子句，是因为在归结时纯文字永远不会被消去，因而用包含它的子句进行归结不可能得到空子句。删除永真式是因为永真式对子句集的不可满足性不起任何作用。删除被类含的子句是因为被类含子句被类含它的子句所逻辑蕴含，故它已是多余的。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 删除策略有如下特点：删除策略的思想是及早删除无用子句，以避免无效归结，缩小搜索规模；并尽量使归结式朝“小”（即元数少）方向发展。从而尽快导出空子句。删除策略是完备的。即对于不可满足的子句集，使用删除策略进行归结，最终必导出空子句。定义一个归结策略是完备的，如果对于不可满足的子句集，使用该策略进行归结，最终必导出空子句。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 2.支持集策略支持集策略：每次归结时，两个亲本子句中至少要有一个是目标公式否定的子句或其后裔。这里的目标公式否定的子句集即为支持集。支持集策略有如下特点：这种策略的思想是尽量避免在可满足的子句集中做归结，因为从中导不出空子句。而求证公式的前提通常是一致的，所以，支持集策略要求归结时从目标公式否定的子句出发进行归结。所以，支持集策略实际是一种目标制导的反向推理。支持集策略是完备的。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.线性归结策略线性归结策略：在归结过程中，除第一次归结可都用给定的子句集S中的子句外，其后的各次归结则至少要有一个亲本子句是上次归结的结果。线性归结的归结演绎树如图33所示.线性归结策略的特点是：不仅它本身是完备的，高效的，而且还与许多别的策略兼容。例如在线性归结中可同时采用支持集策略或输入策略。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 图33线性归结演绎树图34例3.29归结演绎树第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 4.输入归结策略输入归结策略：每次参加归结的两个亲本子句，必须至少有一个是初始子句集S中的子句。可以看出，例3.29中的归结过程也可看作是运用了输入策略。输入归结策略的特点是：输入归结策略实际是一种自底向上的推理，它有相当高的效率。输入归结是不完备的。输入归结往往同线性归结配合使用，组成所谓线性输入归结策略。当然，进一步还可以与支持集策略结合。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 5.单元归结策略单元归结策略：在归结过程中，每次参加归结的两个亲本子句中必须至少有一个是单元子句。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 6.祖先过滤形策略祖先过滤形策略：参加归结的两个子句，要么至少有一个是初始子句集中的子句；要么一个是另一个的祖先（或者说一个是另一个的后裔）。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.4.3 归结策略的类型归结策略的类型上面我们介绍了一些常用的归结策略。除此而外，人们还提出了许多别的策略，如锁归结、语义归结、加权策略、模型策略等。锁归结的思想是：用数字1,2,3,对各子句中的文字进行编号，使互不相同的文字或相同文字的不同出现具有不同的编号，这种编号就称为文字的锁，如1P3Q和5P9P中的1,3,5,9就都是锁。这样，归结就可用锁来控制。具体做法是：每次归结，参加归结的文字必须分别是所在子句中编号最小者。例如，有子句1P2Q和3P4Q，则只能对P、P作归结。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 语义归结的基本思想是将子句集S中的子句分成两组，只考虑组间子句的归结。加权策略是对子句或其中的项赋予相应的权值，以反映子句或项在实际问题中的某种程度，这样，归结就可用权值来控制。如给出某种顺序或限制。虽然归结策略很多，但归纳起来，大致可以分为三类：(1)简化性策略。(2)限制性策略。(3)有序性策略。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 有了归结策略后，本节开始所给的归结反演一般算法可改为：步1将子句集S置入CLAUSES表；步2若空子句NIL在CLAUSES中，则归结成功，结束。步3按某种策略在CLAUSES表中寻找可归结的子 句 对，若 存 在 则 归 结 之，并 将 归 结 式 并 入CLAUSES表，转步2；步4归结失败，退出。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 该程序的目标子句是prove(F,S)，其中S为前提，F为 要 证 明 的 结 论 的 否 定。程 序 运 行 时，谓 词union(F,S,FS)首先把待证结论的否定子句F与前提子句S合并为FS。接着，谓词proof(FS)对子句集FS进行归结反 演，试 图 推 出 空 子 句 。proof又 调 用 谓 词resolution进行归结。proof的第一个子句是归结反演的终结条件；第二个子句是归结反演的递归操作。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.7 非归结演绎推理非归结演绎推理 3.7.1Bledsoe自然演绎法这种自然演绎法采用多条推理规则（当然是一些特定形式的规则），试图模拟人脑的推理证明方式，由前提推证结论。著名的IMPLY系统就是一个Bledsoe自然演绎推理的定理证明系统。它是Bledsoe等于1975年在Texas大学研制的。这是一种效率较高的定理证明系统。例如微积分中连续函数的和仍连续的定理，仅用27步就得到了证明。但用归结法时，推出了10万个子句还尚无结果。第第3章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理 3.7.2基于规则的演绎推理这是另一种非归结推理。这种推理将前提谓词公式集合分为规则和事实两部分，并以特定的形式加以表示，然后，用规则与事实进行匹配，进行演绎推理。基于规则的演绎推理系统，称为规则演绎系统。实际上它是一种基于谓词逻辑的产生式系统。规则演绎系统又分为前向演绎系统、后向演绎系统和双向演绎系统。前向系统基于一组前向规则（称为F-规则），从事实出发进行推理；后向系统基于一组后向规则（称为B-规则），从目标出发进行推理；双向系统则同时基于F-规则和B-规则，同时从事实和目标出发进行推理。