【教学课件】第3章谓词逻辑和归结原理.ppt

第 3 章 谓词逻辑和归结原理,逻辑:推理的理论和根据.逻辑的分类,经典逻辑和非经典逻辑 命题逻辑和谓词逻辑,3.1 命题逻辑1。什么是命题？2。什么是命题连接词？3。什么命题公式（Well-formed formula,WFF）？4。什么是命题演算语句解释？5。什么是命题演算语句在某解释下的真值？6。什么是命题演算语句的真值表？7。什么是恒真的命题公式?8。如何进行命题逻辑的推理,命题逻辑的推理规则符号和语句定义:命题演算符号包括命题符号:P,Q,R,S,.真值符号:true,false 连接词:,定义:命题逻辑公式（Well-formed formula,WFF）利用命题演算符号，真值符号和逻辑连接词组成 的合法符号串。,合取项(conjunct)析取项（disjunct）蕴涵式（implication）前提（premise）,前项(antecedent)结论（conclusion）,后项（consequent）命题语句的例 P,Q,R,P,Q,PQ,PQR,PQ,PQ R(PQ)R PQ R,命题语句就是一个符号串，只有对串中的命题符号指定了真假值之后，这个语句才具有实际意义。命题演算的语义 由单个逻辑运算符连接的简单语句的语义定义：命题语句的语义 对每一个命题指定其真假值。按由单个逻辑运算符连接的简单语句的语义递归地求出整个语句的真假值。解释：对命题指定其真假值,同一个命题语句在不同的解释之下有不同的真值。如果一个命题语句具有n 个命题，则其具有 2n种不同的解释 真值表：设 s 使一个命题语句，s 的真值表是对s 的所有可能解释的真值。,P,Q,FFTT,FFTT,FFTT,P Q,P,P,Q,PVQ,PQ,(PVQ)PQ,TTFF,TFTF,FFTT,TFTT,TFTT,TTTT,命题逻辑的等价命题逻辑中常用的等价公式,命题逻辑的推理规则,推理规则是用一些命题公式A1,A2,推导出另外一些命题公式B1,B2,附加:A=AB简化:AB=A假言推理:AB,A=A拒取式:AB,B=A析取三段论:AB,A=B假言三段论:AB,BC=AC,命题逻辑的推理规则,例 1证明(PQ)，(PR)，(ST),(SR),TQ 1.ST 前提引入 2.T 前提引入 3.S 1,2,拒取规则4.SR 前提引入 5.R 3,4 假言推理6.P R 前提引入7.P 5，6；拒取规则8.PQ 前提引入 9.Q 7,8,析取三段论,命题逻辑的推理规则,写出对应下面推理的证明如果今天下雨.则要带伞或雨衣,如果走路上班,则不带雨衣,今天下雨,走路上班,所以带伞.P:今天下雨 Q:带伞 R:带雨衣 S:走路上班,命题逻辑的推理规则,P(QR)，(SR)，P,SQ 1.P(QR)前提引入 2.P 前提引入 3.QR 1,2,假言推理4.SR 前提引入 5.S 前提引入 6.R 4,5,假言推理7.Q 3,6,析取三段论,命题逻辑归结方法,前面给出的命题逻辑的证明过程需要很多思考过程，人可以用来实施推理，但却不适用于计算机。本节我们介绍一中推理方法归结方法，它以机械的方式实施推理，容易使用计算机实现，我们先介绍它的简单情形，即命题逻辑的归结，然后在下一节介绍谓词逻辑归结。命题逻辑证明过程之所以复杂的一个重要原因是命题公式的形式是各种各样的。证明系统必须有处理各种各样命题公式的能力。为了简化命题公式的形式，人们提出了一种简单而又有足够表达能力的形式，这就是子句。,命题逻辑归结方法,为叙述方便，我们把命题原子称作正文字，例如P,Q,R.,等等，把带有非符号的命题原子叫做负文字，例如P,Q,R.,等等，把正文字和负文字统称为文字。单个文字，文字的析取构成的命题逻辑公式叫做子句。例如，P,Q,P Q R都是子句。,命题逻辑归结方法,一个命题逻辑公式可以采用如下方式转换成等价的子句的合取形式,即合取范式：1.利用等价公式 PQ=(PQ)(QP)和PQ=PQ删去公式中的符号和符号.2.利用De Morgan 律把所有的否定符号移到每个原子之前.3.利用分配律得到子句的合取形式,命题逻辑归结方法,例 把命题逻辑公式(PQ)(Q R)转换成等价的子句的合取形式.(PQ)(Q R)=(PQ)(Q R)=(PQ)(Q R)=(PQ)(Q R)=(PQ)(PQ R)上式即为子句的合取形式,命题逻辑归结方法,命题归结式设c1,c2是两个子句，c1=L1D1,c2=L2D2,其中L1=L2，L1，L2也称作互补文字，D1和D2 为子句则D1D2称作c1,c2的归结式，记为R(c1,c2),c1,c2称做是归结式的亲本子句。例如，设c1,c2是两个子句，c1=PQ,c2=PR S,则P和P为互补文字,c1,c2的归结式是QR S.,命题逻辑归结方法,在利用归结推导证明某一逻辑结果时，我们采用如下的归结反驳证明方法。设F=f1,f2,fn是命题逻辑公式集合，g 是命题逻辑公式，为了证明从 F能推导出 g，我们先把逻辑公式f1,f2,fn转换成子句或子句集，把g 的否定g 也转换成子句或子句集，然后把这些子句放在一起，组成一个子句集，在此子句集上应用归结，把所得到的归结式不断地加入到子句集中，继续进行归结，当子句集中包含空子句时，则认为是已经从F推导出g.这种归结反驳证明的核心思想是反证法，空子句表示矛盾。在证明过程中用表示。如果把要证的结论的否定加入到前提集合中能导出矛盾，则证明了该结论。理论上可以证明，命题中归结反驳证明方法是可靠的。,命题逻辑归结方法,例：证明(P Q)(Q P)前提集合F=(P Q),结论=(Q P)。F中命题公式转换成的子句集是 PQg 转换成的子句集是Q,P 把上述子句集组合在一起，得到初始子句集=PQ,Q,P,命题逻辑归结方法,以下为归结过程1.PQ2.Q3.P 1,2 归结4.Q 2,4 归结5,3.2 谓词逻辑基础 3.2.1 谓词的基本概念 个体词:表示具体的客体,如:小王,工程师,8,自然数.谓词:表示个体的性质和个体间的关系,小王是个工程师 8 是自然数 变量符号：v1,w2,table3,常量符号:A,Dog,Wang1.函数符号:f(x),g(u,v),定义：符号和项由变量符号，常量符号，函数符号和逻辑常量组成的合法字符串。定义：谓词和原子语句谓词是取值范围为0（假），1（真）的函数。单独一个谓词构成的语句为原子语句。例:P(x),Q(x,y),R(X,b),量词全称量词 对于日常生活和数学中出现的“一切的”、“任意的”、“所有的”、“每一个”、“都”、“凡”等词统称为全称量词，用符号“”表示。并用x，y表示个体域中的所有个体，用（x）F（x），（y）F（y）等表示个体域中的所有个体具有性质F。存在量词 对日常生活和数学中常用的“存在”、“存在一个”、“有一个”、“至少有一个”、“有些”、“有的”等词统称为存在量词，用符号“”表示。并用x，y表示个体域中有的个体，用（x）F（x），（y）F（y）等表示个体域中有的个体具有性质F。,量词的例,例 将下面的命题符号化：（1）所有人都是要死的。（2）有的人活到100岁以上。其中：个体域D为人类集合。解 令R（x）：x是人,P(x):x要死的；Q（x）：活到100岁以上。则（1）可符号化为：x（R（x）P（x）（2）可符号化为 x（M（x）Q（x）,使用量词需要注意,在不同的个体域中,符号化的形式可能不一样.使用量词需要注意:多个量词同时出现时,不能颠倒它们的次序例如:“对于任意 x,存在 y,使得 x+y=5”,设 P(x,y)为 x+y=5,符号化为x yP(x,y),为真命题.但是,y x P(x,y),“存在 y,对于任意 x,使得 x+y=5”,为假命题,1。什么是一阶逻辑的全称量词？如何表示？2。什么是一阶逻辑的存在量词？如何表示？3。什么是一阶逻辑公式的解释？4。什么是一阶逻辑公式的在解释下的真值？举例说明。5。给出一个恒真的一阶逻辑公式的例。,3.2.2 一阶谓词逻辑定义：谓词演算语句（递归定义）利用原子语句，合取，析取，否定，蕴涵，全称，定量等符号构成的合法字符串。谓词演算的语义定义：谓词演算语句的解释 由一个论域 D 和一组指定组成 谓词语句在解释下的真值,在谓词演算中使用推理 一个解释由一个论域 D 和一组指定组成定义：满足，模型，有效，不一致 如果一个解释 I 使语句 s 取值为真，则称解释I满足s,也称I是s的模型，如果语句s对所有解释都取值为真，则s称为是有效的（valid）,如果语句s对所有解释都取值为假，则s称为是不一致的（inconsistent）,定义：证明过程 利用逻辑蕴涵推出新语句的过程，推导出的结果称为推导结果,给出如下两个公式：1)A=x(P(f(x)Q(x，f(x)2)B=x y R(x，y)给出如下的解释I：D=2，3 f(2)f(3)3 2 P(2)P(3)Q(2，2)Q(2，3)Q(3，2)Q(3，3)0 1 1 1 1 1 R(2，2)R(2，3)R(3，2)R(3，3)1 0 0 1,解：A(P(f(2)Q(2，f(2)(P(f(3)Q(3，f(2)(P(3)Q(2，3)(P(2)Q(3，3)(11)(01)1所以公式在解释I下为真B(R(2,2)R(2，3)(R(3,2)R(3，3)11 1所以公式在解释I下为真.,判断公式类型：（1）xyP(x，y)Q，x，y的个体域为R，P(x，y)：x=y；Q是命题变元。解：xy(x=y)是真命题当Q=1时，该公式为真当Q=0时，该公式为假因此，该公式是可满足公式。,（2）(P(x，y)P(x，y)(Q Q)解：因为R中任意取定的一组x，y均使(x=y)(x=y)是一真命题，而Q Q是一重言式，所以对于任一组指派，(P(x，y)P(x，y)总为真，故该公式为永真公式。（3）xy(P(x，y)P(x，y)解：因为R中任意取定的一组x，y，公式 P(x，y)P(x，y)总为假，所以该公式为永假公式。,3.2.3 谓词演算和推理,1.谓词演算公式 约束变量换名规则(Q(x)P(x)(Q(y)P(y)(Q(x)P(x,z)(Q(y)P(y,z)2.量词否定等值(1）（x）G（x）（x）G（x）（2）（x）G（x）（x）G（x）3.量词分配等值(1)（x）（G（x）H（x）（x）G（x）（x）H（x）(2)（x）（G（x）H（x）（x）G（x）（x）H（x）,3.2.3 谓词演算和推理,消去量词等值 x A（x）A（a1）A（a2）A（an）x A（x）A（a1）A（a2）A（an）。量词辖域收缩与扩张（1）（x）（G（x）B）（x）G（x）B（2）（x）（G（x）B）（x）G（x）B（3）（x）（G（x）B）（x）G（x）B（4）（x）（BG（x）B（x）G（x）（5）（x）（G（x）B）（x）G（x）B（6）（x）（G（x）B）（x）G（x）B（7）（x）（G（x）B）（x）G（x）B（8）（x）（BG（x）B（x）G（x）,3.2.3 谓词演算和推理,前束范式定理2.4.1 对任意一个谓词公式都可以化为与它等价的前束范式。首先利用等价公式将谓词公式中的联结词，去掉。其次利用量词的转化律将量词前面的否定深入到谓词前面，在利用改名和代入规则以及量词辖域扩张的公式将量词移到全式的最前面，这样便得到公式的前束范式。,3.2.3 谓词演算和推理,求(（x）P（x，y）（y）Q（y）)（x）R（x，y）的前束范式.(（x）P（x，y）（y）Q（y）)（x）R（x，y）(（x）P（x，z）（y）Q（y）)（x）R（x，z）（x）(P（x，z）（y）Q（y）)（t）R（t，z）（x）（y）(P（x，z）Q（y）)（t）R（t，z）（x）（y）(P（x，z）Q（y）)（t）R（t，z）)（x）（y）（t）(P（x，z）Q（y）)R（t，z）),3.2.3 谓词演算和推理,谓词推理1全称指定规则（简称US规则）2全称推广规则（简称UG规则）3存在指定规则（简称ES规则）4存在推广规则（简称EG规则）,3.2.3 谓词演算和推理,1全称指定规则（简称US规则）这条规有下面两种形式：(1)x P（x）P（y）(2)x P（x）P（c）其中，P是谓词，（1）中y为任意不在P（x）中约束出现的个体 变元；（2）中c为个体域中的任意一个个体常元。,3.2.3 谓词演算和推理,3存在指定规则（简称ES规则）x P（x）P（c）其中，c为个体域中使P成立的特定个体常元。必须注意，应用 存在指定规则，其指定的个体c不是任意的。,2全称推广规则（简称UG规则）P（y）x P（x）,4存在推广规则（简称EG规则）P（c）x P（x）其中，c为个体域中的个体常元，这个规则比较明显，对于某些个体c，若P（c）成立，则个体域中必有x P（x）。,3.2.3 谓词演算和推理,例 20世纪 70 年代的漫画都是日本漫画家创作的,这幅画是20世纪 70 年代的作品,因此,这幅画是日本漫画家创作的.P(x):20世纪 70 年代的漫画,Q(y):这幅画是日本漫画家的作品.a:一幅漫画前提:x(P（x）（y）Q（x）),P(a)结论:Q(a)证明 1.x(P（x）（y）Q（x）)前提引入 2.P(a)前提引入 3.P（a）Q（a）全称指定 4.Q(a)假言推理,3.2.4 谓词知识表示,逻辑是一中重要的知识表示方法.谓词表示的优点 1.表达能力强.2.谓词的真值可以随参数的变化而变化 3.可以在不同的知识之间建立起联系,3.2.4 谓词知识表示,谓词逻辑获得广泛应用的原因1.谓词逻辑与数据库有密切联系.2.一阶谓词逻辑具有完备的推理算法.3.谓词逻辑具有可靠的数学基础.4.能够保证新增添的知识具有一致性.,3.2.4 谓词知识表示,例 一个房间里有一个机器人Robot,一个积木块Box,两个桌子A 和B,用逻辑描述从初始状态到目标状态的操作过程.谓词:Table(A)A是桌子EmptyHanded(Robot)机器人的手是空的At(Robot,A)机器人Robot在A旁Holds(Robot,Box)机器人Robot拿着BoxOn(Box,A)积木块Box在A上初始状态EmptyHanded(Robot)On(Box,A),3.2.4 谓词知识表示,Table(A)Table(B)目标状态EmptyHanded(Robot)On(Box,B)Table(A)Table(B)机器人的动作的描述,3 部分前提条件增加表删除表例如:机器人把Box从A桌移到B桌前提条件 Holds(Robot,Box)增加表 On(Box,B)删除表 On(Box,A),3.3 谓词归结原理,Skolem 标准型 要想在谓词逻辑中应用归结原理，需要首先把谓词逻辑公式转换成子句。因为谓词逻辑包含谓词和量词，这种转换要比命题逻辑中公式的转换复杂得多，下面我们介绍转换的步骤：1.利用等价公式 PQ=(PQ)(QP)和PQ=PQ删去公式中的符号和符号，这个步骤与命题逻辑的对应处理方式相同。2.利用De Morgan 律把所有的否定符号移到每个原子之前.,3.3 谓词归结原理,3.把变量标准化.因为根据变量的改名规则，量词所约束的变量可以在量词作用范围内用另外变量代替。我们可以对变量适当地改名,使每一个量词所约束的变量都有不同的名字.例如,谓词公式（x）P（x）(x)Q（x）改写成（x）P（x）(y)Q（y）.4.删除公式中的存在量词.例如,谓词公式（x)(y)P（x,y)在删去存在量词之后,变成（x)P（x,f(x),在删去存在量词之后,这个存在量词所约束的变量的每次出现都用一个函数代替,这个函数的自变量是约束范围包含删除的存在量词的所有全称量词限制的变量.这个函数也叫做 Skolem函数.把删除存在量词,将存在量词限制的变量用对应的Skolem函数代替的过程叫做Skolem化过程.结果叫做Skolem范式.,3.3 谓词归结原理,例 将下式化为Skolem标准型:(（x)(y)P(a,x,y)(x)(（y）Q(y,b)R(x)(（x)(y)P(a,x,y)(x)(（y）Q(y,b)R(x)（x)(y)P(a,x,y)(x)(（y）Q(y,b)R(x)（x)(y)P(a,x,y)(x)(（y）Q(y,b)R(x)（x)(y)P(a,x,y)(（y）Q(y,b)R(x)（x)(y)P(a,x,y)(（z）Q(z,b)R(x)（x)(y)（z）(P(a,x,y)Q(z,b)R(x)（x)（z）(P(a,x,f(x)Q(z,b)R(x)（x)(P(a,x,f(x)Q(g(x),b)R(x),3.3 谓词归结原理(子句集),文字 我们把命题原子称作正文字，例如P(x),Q(y,b),R(w,c).,等等，把带有非符号的命题原子叫做负文字，例如P(y),Q(a,b),R(x,y,z).,等等，把正文字和负文字统称为文字。子句 单个文字，文字的析取构成的命题逻辑公式叫做子句。例如，P,Q(x),P(x)Q(y,b),都是子句。子句集 若干子句的集合.一个命题逻辑公式可以采用如下方式转换成等价的子句的合取形式,即合取范式：1.利用等价公式 PQ=(PQ)(QP)和PQ=PQ删去公式中的符号和符号.2.利用De Morgan 律把所有的否定符号移到每个原子之前.3.利用分配律得到子句的合取形式,3.3 谓词归结原理(子句集),把公式变换成Skolem标准型.5.把Skolem标准型中子句提出.表示为集合形式.定理 3.1 公式G是不可满足的,当且仅当其子句集S是不可满足的,3.3 谓词归结原理(替换与合一),在命题逻辑归结中,需要两个子句有互补文字,这两个文字除了否定符号之外是完全相同的.但在谓词逻辑中包含变量,而变量可以指定成其他任何常量,变量,或者函数项,可以在指定后再实施归结,因此即使两个项不完全相同,也可能进行归结.例如,设有谓词逻辑子句c1和 c2，c1=P(x)Q(x,y)c2=P(f(a)R(x,b),表明上看来没有互补文字,但是,如果把c1和 c2中的x都指定成 f(a),则有互补对 P(f(a)和 P(f(a),这时c1和 c2 就可以归结得到 Q(f(a),y)R(f(a),b),这种为变量的指定称为替换,本节我们先介绍替换.,3.3 谓词归结原理(替换与合一),替换是如下形式的偶对组成的集合:s=t1/v1,t2/v2,tn/vn,其中t1,t2,tn是项,v1,v2,vn是彼此不同的变量,ti中不包含变量vi.例如,下面的4个偶对集合是4个替换:s1=z/x,w/y s2=A/y s3=g(z)/x,A/y s4=C/x,A/y 把替换s用于表达式E是把E中变量vi的每次出现都用对应的项ti 代替(i=1,2,n),成为表达式E的替换例，记为Es.例如，设E=P(x,f(y),B),则Es1=P(z,f(w),B)Es2=P(x,f(A),B)Es3=P(g(z),f(A),B)Es4=P(C,f(A),B),3.3 谓词归结原理(替换与合一),设s1和s2 是两个替换，s1=t1/x1,t2/x2,tn/xn s2=u1/y1,u2/y2,un/yn 我们可以利用s1和s2组合产生一个新的替换，这种组合相当于引进替换中的一种运算，记为s1s2,其结果是把s2用在s1的所有的项ti 上(i=1,2,n)，然后把s2中加进去，得到 t1s2/x1,t2s2/x2,tns2/xn,u1/y1,u2/y2,um/ym再删除一些不符合替换要求的偶对:tis2=xi,s2变量在s1出现的偶对。例如，设：s1=f(y)/x,z/y,s2=a/x,b/y,y/z 则 从集合中 f(b)/x,y/y,a/x,b/y,y/z 删除y/y，a/x，b/y,得到s1s2=f(b)/x,y/z,3.3 谓词归结原理(替换与合一),替换的复合运算满足结合律，不满足交换律。,3.3 谓词归结原理(替换与合一),设E1,E2,En是一个表达式集合，如果存在一个替换 s，把s用于这个表达式集合的替换例集合满足E1s=E2s=,=Ens,则称该表达式集合是可合一的，而s称为该表达式集合的合一替换。例如，设E1=P(x,f(y),B),E2=P(x,f(B),B),s=A/x,B/y,则容易验证E1s=E2s=P(A,f(B),B)因此E1和E2是可合一的。尽管这个替换s可以使E1和E2合一，但s并不是最简单的。在谓词逻辑归结中，我们总希望使用最简单的合一。因此下面给出最一般合一的概念。设设E1,E2,En是一个表达式集合，g是该表达式集合的一个合一替换,如果对任何合一替换s,都有替换s,满足s=gs，则称g是E1,E2,En的最一般合一替换。在我们上述的例子中，最一般合一替换是个g=B/y,s=g A/x.,3.3 谓词归结原理(替换与合一),求最一般合一算法1.令W=F1,F2令k=0,W0=W,s0=如果Wk已合一,停止,sk=mgu,否则,找不一致集合Dk,4.如果Dk中存在元素vk和tk,并且vk不出现在tk中,转5,否则不可合一.5.sk+1=sktk/vk,Wk+1=Wktk/vk6,k=k+1,转3.,3.3 谓词归结原理(替换与合一),例,设f1=P(a,x,f(g(y),F2=P(z,f(a),f(u),3.3 谓词归结原理(归结式),谓词逻辑归结式设c1,c2是两个子句，为叙述方便，我们假定子句都写成文字集合的形式，而把这些集合中文字的关系约定为析取。c1=L1D1,c2=L2D2,其中L1，L2是可合一的原子，假设它们的最一般合一是s，D1和D2 为子句则c1,c2的归结式 r 为：(c1 L1)(c2L2)s在对子句实施归结之前，为了避免不必要的混淆，我们对子句中的变量进行改名，使得各子句中的变量都使用不同的名字。例如，假设我们想要对两个子句 P(x)Q(f(x)和 R(g(x)Q(f(A)实施归结，我们先把第二个子句中变量进行改名，得到R(g(y)Q(f(A),然后通过归结得到P(A)R(g(y),这种变量改名的过程也叫做变量的分离标准化。,3.3 谓词归结原理(归结式),例(1)c1=P(x)Q(x,y)和 c2=P(a)R(b,z)它们的归结式R(c1,c2)=Q(a,y)R(b,z)例(2)c1=P(x,y)Q(x)R(x)和 c2=P(a,z)Q(b)它们的归结式R(c1,c2)=Q(a)R(a)Q(b)或者 P(b,y)R(b)P(a,z),3.3 谓词归结原理(归结过程),谓词逻辑中归结方法的主要思想与命题逻辑相同。假设我们想从公式集合SF=f1,fn出发证明公式 g,SF称为前提集合，g称为结论，我们先把f1,fn 和 g 转换成子句集 Cf1,Cfn 和 Cg,设 SC=Cf1,Cfn Cg为初始子句集，然后在SC的子句间实施归结，不断地加入新的归结式，然后继续归结，当子句集中出现了空子句时，我们就证明了SF g,即证明了g是SF的逻辑结果。,3.3 谓词归结原理(归结过程),例 假设任何任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有的考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。求证：张是快乐的。R1:任何任何通过计算机考试并获奖的人都是快乐的（x)(Pass(x,computer)Win(x,prize)Happy(x)R2:任何肯学习或幸运的人都可以通过所有的考试，（x)（y)(Study(x)Lucky(x)(Pass(x,y)R3:张不肯学习但他是幸运的 Study(zhang)Lucky(zhang)R4:任何幸运的人都能获奖（x)(Lucky(x)Win(x,prize),3.3 谓词归结原理(归结过程),要证的结果：张是快乐的。Happy(zhang)转换为子句 Pass(x,computer)Win(x,prize)Happy(x)Study(y)Pass(y,z)Lucky(u)Pass(u,v)Study(zhang)Lucky(zhang)Lucky(x)Win(x,prize)Happy(zhang),3.3 谓词归结原理(归结过程),8.Pass(w,computer)Happy(w)Lucky(w)1,6 w/x9.Pass(zhang,computer)Lucky(zhang)7,6 zhang/w10.Pass(zhang,computer)9,511.Lucky(zhang)10,3 zhang/u,computer/v12.11,5,3.3 谓词归结原理(控制策略),1.最简单的控制方式是宽度优先方式，我们把归结的初始集合S中的子句叫做0层子句集，先在0层子句集中的字句实施归结，考虑0层子句集中的所有子句对，把所有能归结的子句对都实施归结，产生所有的归结式加入到0层子句集中，得到 1 层子句集。然后考虑1层子句集中的所有子句对，把所有能归结的子句对都实施归结，产生所有的归结式加入到1层子句集中，得到 2 层子句集。按照上述方式一层一层地进行归结，直至到包含空子句的某一层为止。显然这种宽度优先方式所产生的无用的归结式最多，效率因此也最低。但是宽度优先归结是完备的，即如果从子句S能推出矛盾，则宽度优先归结一定能得到空子句。,3.3 谓词归结原理(控制策略),例4.4 考虑如下谓词逻辑证明问题：所有能读书的人都是识字的，海豚不识字，某些海豚是有智能的，证明有些动物 有智能但不会读书。为描述这个推理问题，我们引进四个谓词：R(x)：x能读书，L(x)：x识字，D(x)：x是海豚，I(x)：x是有智能的。利用上述谓词，我们可以把例子提出的问题描述成谓词逻辑公式：,3.3 谓词归结原理(控制策略),1 所有能读书的人都是识字的 f1=(x)R(x)L(x)2 海豚不识字 f2=(x)D(x)L(x)3 某些海豚是有智能的 f3=(x)D(x)I(x)4有些动物有智能但不会读书 g=(x)I(x)R(x)我们希望从f1,f2,f3证明出 g,首先把上述谓词公式转换成字句，并进行变量分离标准化，对应的数字标出了从谓词公式得到的字句，从 f3 可以得到两个字句（3a）和（3b）,子句中的A是通过Skolem化得到的。(1)R(x)L(x)(2)D(y)L(y)(3a)D(A)(3b)I(A)把要证的结论的否定g转换成子句为：(4)I(z)R(z)在上述子句间实施归结，不断地加入新的归结式，然后继续归结，,3.3 谓词归结原理(控制策略),3.3 谓词归结原理(控制策略),控制策略的目的是避免多余的归结式的出现,提高归结的效率.1.解决归结过程中组合爆炸问题 2.减少多余的归结式.3.删除不必要的子句,对参加归结的子句加以限制,3.3 谓词归结原理(控制策略),删除策略 归类(subsume)设有两个子句C和D,如果有替换使得 Cs 是D的子集,则称子句C把子句D归类.例,设C=P(x),D=P(a)Q(y)则子句C把子句D归类.删除策略:1.含有恒真式的子句.2.被子句集中其他子句归类的子句.例如,初始子句集为P(a)Q(y),P(a)Q(y),P(x),Q(y),3.3 谓词归结原理(控制策略),2.当我们使用反证法进行推理时，我们把结论g的否定g加入到前提集合SP中，并想从由此得到的集合中推出矛盾。但是，前提集合SP一般说来是相容的，仅利用从前提集合一般说来不能推出矛盾。要想推出矛盾，必须使用g。因此g在反证法中有着特殊的作用。把这个规律应用在归结方法中，我们把由g产生的子句，或g产生的子句与其他子句产生的归结后裔叫做支架集。支架集归结要求在归结过程中选择亲本子句时，两个子句至少有一个是取自支架集。支架集归结的效率比宽度优先归结要高，并且是完备的。,3.3 谓词归结原理(控制策略),例如,前提子句集为P Q,P R,Q R要证的目标是R采用支架集的归结过程如下:R 目标的否定Q R 前提Q 1,2P Q 前提5 P 3,4P RP 1,68 5,7 书上的例有问题,3.3 谓词归结原理(控制策略),语义归结策略利用一个解释把子句分成两个子句集,限制同集合内的子句的归结把原子谓词排序,约定归结时,其中一个子句的归结文字只能是该子句的最大文字.例如,前提子句集为 P Q R,P R,Q R,R取解释 I=P,Q,R,规定PQR则 I 将初始子句集分成两个子句集,S1和S2,S1=P R,Q R,S2=P Q R,R1.P Q R S22.P R S13.Q R S14.Q R S2,from 1,25.R 3,46.R S27.5,6,3.3 谓词归结原理(控制策略),与支架集策略一样,语义归结的效率比宽度优先归结要高，并且是完备的。语义归结的关键是如何寻找恰当的解释,把子句分成两个子句集,3.3 谓词归结原理(控制策略),线性归结策略线性归结策略首先从子句集中选取一个子句C0开始归结,C0称为顶子句,然后,每次归结都使用C0的后继子句,在得到C0的后继子句Ci后,立即同另一个子句进行归结,得到Ci+1,如下图所示,C0,C1,B0,C2,B0,B0,.,3.3 谓词归结原理(控制策略),单元归结策略 只由一个文字构成的子句叫单元子句,如果归结过程中两个亲本子句至少有一个是单元子句,则所得归结式比较简单,相当于把另外一个子句删除一个文字,因此,如果子句集中有单元子句,我们应尽可能优先使用单元子句实施归结.如果归结过程中两个亲本子句至少有一个是单元子句,这种归结称做单元归结.例如,图4.8 所示归结也是单元归结.显然,仅使用单元归结并不能保证在矛盾的子句集中一定能得到空子句,因此单元归结是不完备的,但是我们可以把优先使用单元归结作为一个原则,以提高归结方法的效率.例如,前提子句集为 P Q R,P R,Q R,R归结过程先选择 R.,3.3 谓词归结原理(控制策略),输入归结策略 要求在归结过程中,每一次归结的过程中两个子句必须有一个是初始子句集中的子句.输入归结是不完备的.,设 F是谓词语句集合，g 是一个谓词语句，语句序列 f1,f2,fn称做是由F出发而得到 g 的一个证明过程，如果：1。fi 是F中的公式，或者2。fi 是对 fj和fk使用推导公式所得到的逻辑结果。3。fn=g这时，我们也称之为语句集合F推导出g。例：设 F是谓词语句集合，g 是一个谓词语句，F=(PQ),(PR),(Q S),g=SR 证明语句集合F推导出g。我们可以使用如下的语句序列 1。PQ（语句1取自前提集合）2。P Q(语句2是语句1的等价公式)3。Q S（语句3取自前提集合）,4。P S（由 2，3，使用蕴涵的传递性）5。S P(由4，语句5是语句4的等价形式)6。PR（语句6取自前提集合）7。S R（由 5，6，使用蕴涵的传递性）8。SR(由7，语句8是语句7的等价形式)语句8.也就是要证明的公式g.定理：设 F是命题语句集合，g 是一个命题语句，从语句集合F推导出g的充分必要条件是g是F 的逻辑结果。,定义：逻辑结果 设S是一个语句集，X 是一个语句，如果 S 所有模型都是X的模型，则称X是S的逻辑结果。定义：可靠性与完备性 设S是一个语句集，p 是证明过程。如果从S出发利用p得到的语句都是S的逻辑结果，则称p是可靠的。如果S的逻辑结果都可以从S出发利用p推导得到，则称p是可靠的。,定义：假言推理，拒式假言推理，与删除，与引入，全称例化 假言推理：P,P-Q,Q拒式假言推理：Q,P-Q,P,与删除：PQ=P,Q与引入：P,Q=PQ,例。man(x):x 是人 mortal(x):x 必定要死的 man(Socrates):苏格拉底是人,全称例化,假言推理,合一算法 unification为什么我们需要合一算法,(xA),我们必须知道 P(x)和 P(a)是可以通过替换变为相同的表达式替换（substitution）:由偶对ti/vi 做成的集合 t1/v1,t2/v2,tn/vn 其中，t1,t2,tn 是项,v1,v2,vn 是变量.,(P(x)Q(x),P(a),Q(a),替换的结果：设E是谓词语句，s是替换，对E使用替换的结果是 把E中出现的所有变量用对应的项代替，其结果记为Es.The result of using a substitution s to a expression E is such a expression that each occurrence of a variable have the same term substituted for it,the result is denoted by Es.例如:E=Px,f(y),B,s1=z/x,w/y Es1=Pz,f(w),B,替换的复合：设s1 和s2 是两个替换,s1=t1/v1,t2/v2,tn/vn s2=w1/y1,w2/y2,wn/yn,s1和s2的复合是把 s2用于s1的项，在产生的偶对集合中加上s2 的变量不在s1中的偶对。The composition of s1 and s2 is a substitution,which is obtained by applying s2 to the terms of s1 and then adding any pairs of s2 having variables not occurring among the variables of s1例 s1=g(x,y)/z,s2=A/x,B/y,C/w,d/zs1s2=g(A,B)/z,A/x,B/y,C/w,替换的复合具有结合律（associative）:(s1s2)s3=s1(s2s3)但一般说来是不可交换的s1s2s2s1 合一（unification）:设 E1 和 E2 是两个语句,s 是一个替换,如果 E1s=E2s,则 E1 和 E2 称做是可合一的（unifiable），s 叫做 它们的合一替换（unifier）.例 E1=Px,f(y),B,E2=Px,f(B),B,s=A/x,B/y 则 E1s=E2s,s是 E1和 E2合一替换.定义最一般合一替换（The most general unifier,mgu）：设s1 和s2 是两个替换,设 E1 和 E2 是两个语句,g 是它们的一个替换,如果对于它们的任意替换s,均有：s=gs.则称g是最一般合一替换。G=B/y is mgu.,function UNIFY(E1,E2)begin case both E1 and E2 are constants or the empty list:if E1=E2 are then return NIL,else return FAIL E1 is a variable:if E1 occurs in E2,return FAIL else return E2/E1 E2 is a variable,if E2 occurs in E1,return FAIL else return E1/E2 either E1 or E2 are empty then return FAIL otherwisebegin HE1 first(E1);HE2 first(E2);SUB1 UNIFY(HE1,HE2),if SUB1=FAIL,return FAIL TE1 apply(SUB1,tail(T1)TE2 apply(SUB1,tail(T2)SUB 2=UNIFY(TE1,TE2)if SUB2=FAIL,return FAIL else return composition(SUB1 and SUB2)end endend例 E1=(parent X(father X)(mother bill)E2=(parent bill(father bill)Y)mgu(E1,E2)=bill/X,(mother bill)/Y The instance of unification is E2=(parent bill(father bill)(mother bill),1.UNIFY(parent X(father X)(moth