1,第3篇 知识与推理第5章 基于谓词逻辑的机器推理,华南师范大学 教育信息技术学院 郑云翔,2,提纲,一阶谓词逻辑 归结演绎推理 Horn子句归结与逻辑程序,3,一阶谓词逻辑,谓词、函数、量词： 设a1, a2, , an表示个体对象, A表示它们的属性、状态或关系, 则表达式 A(a1, a2, , an)在谓词逻辑中就表示一个(原子)命题。例如： 素数(2), 就表示命题“2是个素数” 好朋友(张三, 李四), 就表示命题“张三和李四是好朋友” 一般地, 表达式 P(x1,x2,xn)在谓词逻辑中称为n元谓词。其中P是谓词符号，也称谓词，代表一个确定的特征或关系(名)。x1,x2,xn称为谓词的参量或者项，一般表示个体,4,一阶谓词逻辑,谓词、函数、量词(续)： f(x1,x2,xn)表示个体变元x1,x2,xn所对应的个体y，并称之为n元个体函数，简称函数 约定用大写英文字母作为谓词符号,用小写字母f, g, h等表示函数符号,用小写字母x, y, z等作为个体变元符号, 用小写字母a, b, c等作为个体常元符号 把“所有”、“一切”、“任一”、“全体”、“凡是”等词统称为全称量词, 记为 x; 把“存在”、“有些”、“至少有一个”、 “有的”等词统称为存在量词, 记为x,5,一阶谓词逻辑,谓词、函数、量词(续)： 对于任意的x, 如果x是人, 则x有名字 存在不是偶数的整数(存在x, x是整数并且x不是偶数) 不存在最大的整数 某些人对某些食物过敏,6,一阶谓词逻辑,谓词、函数、量词(续)： 紧接于量词之后被量词作用(即说明)的谓词公式称为该量词的辖域，例如： (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的辖域,7,一阶谓词逻辑,谓词、函数、量词(续)： 量词后的变元如 x, y中的x, y称为量词的指导变元(或作用变元), 而在一个量词的辖域中与该量词的指导变元相同的变元称为约束变元, 其他变元(如果有的话)称为自由变元, 例如(2)中的x为约束变元, 而y为自由变元, (3)中A(x)中的x为约束变元, 但B(x)中的x为自由变元,8,提纲,一阶谓词逻辑 归结演绎推理 Horn子句归结与逻辑程序,9,归结演绎推理,原子谓词公式及其否定称为文字，若干个文字的一个析取式称为一个子句，1文字子句叫单元子句，不含任何文字的子句称为空子句，记为或NIL 例如下面的析取式都是子句： PQ乛R P(x,y)乛Q(x),10,归结演绎推理,对一个谓词公式G，通过以下步骤所得的子句集合S，称为G的子句集(P102-103) 定理1 把证明一个公式G的不可满足性，转化为证明其子句集S的不可满足性 定义3 子句集S是不可满足的，当且仅当其全部子句的合取式是不可满足的,11,归结演绎推理,命题逻辑中的归结原理： 归结演绎推理是基于一种称为归结原理(亦称消解原理principle of resolution)的推理规则的推理方法 归结原理是由鲁滨逊(J.A.Robinson)于1965年首先提出 它是谓词逻辑中一个相当有效的机械化推理方法。归结原理的出现，被认为是自动推理，特别是定理机器证明领域的重大突破,12,归结演绎推理,命题逻辑中的归结原理(续)： 设L为一个文字，则称L与乛L为互补文字 设C1,C2是命题逻辑中的两个子句，C1中有文字L1，C2中有文字L2，且L1与L2互补，从C1,C2中分别删除L1,L2，再将剩余部分析取起来，记构成的新子句为C12，则称C12为C1,C2的归结式(或消解式)，C1,C2称为其归结式的亲本子句， L1,L2称为消解基 例5.9 设C1=乛PQR, C2=乛QS,于是C1, C2的归结式为乛PRS,13,归结演绎推理,命题逻辑中的归结原理(续)： 推论 设C1,C2是子句集S的两个子句，C12是它们的归结式，则： 若用C12代替C1,C2，得到新子句集S1，则由S1的不可满足可推出原子句集S的不可满足。即 S1不可满足 S不可满足 若把C12加入到S中，得到新子句集S2，则S2与原S的同不可满足。即S2不可满足 S不可满足,14,归结演绎推理,例5.11 证明子句集P乛Q,乛P,Q是不可满足的 证明： (1)P乛Q (2)乛P (3)Q (4)乛Q由(1),(2) (5)由(3),(4),15,归结演绎推理,例5.12 用归结原理证明R是P,(PQ)R,(SU)Q,U的逻辑结果 证明：先把诸前提条件化为子句形式，再把结论的非也化为子句，由所有子句得到子句集S=P,乛P乛QR,乛SQ,乛UQ,U,乛R，然后对该子句集施行归结，归结过程用下面的归结演绎树表示。由于最后推出了空子句，所以子句集S不可满足，即原命题公式不可满足，从而R是题设前提的逻辑结果,16,归结演绎推理,替换与合一：在一阶谓词逻辑中应用消解原理，不像命题逻辑中那样简单，因为谓词逻辑中的子句含有个体变元，这就使寻找含互否文字的子句对的操作变得复杂。例如： C1=P(x)Q(x) C2=乛P(a)R(y) 直接比较，似乎两者中不含互否文字，但如果我们用a替换C1中的x，则得到： C1=P(a)Q(a) C2=乛P(a)R(y),17,归结演绎推理,于是根据命题逻辑中的消解原理，得C1和C2的消解式 C3=Q(a)R(y) 所以，要在谓词逻辑中应用消解原理，则一般需要对个体变元作适当的替换,18,归结演绎推理,例5.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： (1)乛P(x)Q(x) (2)乛P(y)R(y) (3)P(a) (4)S(a) (5)乛S(z)乛R(z),19,归结演绎推理,例5.21(续)： 然后应用消解原理，得 (6)R(a)(2),(3),1=a/y (7)乛R(a)(4),(5),2=a/z (8)(6),(7) 所以S是不可满足的，从而G是A1和A2的逻辑结果,20,归结演绎推理,例5.22 设已知： (1)能阅读者是识字的 (2)海豚不识字 (3)有些海豚是很聪明的 试证明：有些聪明者并不能阅读 证明：首先，定义如下谓词： R(x)：x能阅读 L(x)：x识字 I(x)：x是聪明的 D(x)：x是海豚,21,归结演绎推理,例5.22(续)：然后把上述各语句翻译为谓词公式： (1) x(R(x)L(x) (2) x(D(x)乛L(x) 已知条件 (3) x(D(x)I(x) (4) x(I(x)乛R(x) 需证结论,22,归结演绎推理,例5.22(续)：求题设与结论否定的子句集，得： (1)乛R(x)L(x) (2)乛D(y)乛L(y) (3)D(a) (4)I(a) (5)乛I(z)R(z),23,归结演绎推理,例5.22(续)：归结得： (6) R(a)(5), (4), a/z (7) L (a)(6), (1), a/x (8) 乛D(a)(7), (2), a/y (9) (8), (3),24,提纲,一阶谓词逻辑 归结演绎推理 Horn子句归结与逻辑程序,25,Horn子句归结与逻辑程序,子句的蕴含表示形式： 原子公式及其否定称为文字，现在我们把前者称为正文字，后者称为负文字。例如子句P(x)乛Q(x,y)中P(x)为正文字，乛Q(x,y)为负文字 子句是若干文字的析取，析取满足交换律，所以对于任一个子句我们总可以将其表示成如下形式： 乛Q1乛QnP1Pm (5-1),26,Horn子句归结与逻辑程序,子句的蕴含表示形式(续)： 其中Pi,乛Qj皆为文字，(5-1)式进一步可变形为： Q1Q2QnP1P2Pm (5-2) (5-2)式为一个蕴含式，约定蕴含式前件的文字之间恒为合取关系，而蕴含式后件的文字恒为析取关系，那么(5-2)式又可以改写为 Q1,Q2,QnP1,P2,Pm (5-3) 由于技术上的原因，又将(5-3)式改写为 P1,P2,PmQ1,Q2,Qn (5-4),27,Horn子句归结与逻辑程序,子句的蕴含表示形式(续)： 作为特殊情形，当m=0时，(5-4)式变为： Q1,Q2,Qn (5-4) 它相当于乛(Q1Q2Qn) 当n=0时，(5-4)式变为： P1,P2,Pm (5-4) 它相当于P1P2Pm 这样，对于任一子句，我们总可以把它表示成(5-4)式的形式。子句的这种表示形式称为子句的蕴含表示形式。例如，子句乛P(x)Q(x,y)乛R(y)的蕴含表示形式为 Q(x,y)P(x),R(y),28,Horn子句归结与逻辑程序,Horn子句与逻辑程序： 至多含有一个正文字的子句称为Horn(有些文献中译为“霍恩”)子句。由定义，蕴含型Horn子句有下列三种： (1)PQ1,Q2,Qm 称为条件子句,P称为头部或结论 (2)P 称为无条件句 (3)Q1,Q2,Qm 称为目标子句,Qi称为子目标 可以看出，Horn子句形式简明，逻辑意义清晰，更重要的是Horn子句的消解过程可与计算机程序的执行过程统一起来,29,Horn子句归结与逻辑程序,例5.31 证明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)(目标子句),30,Horn子句归结与逻辑程序,从目标子句出发，采用线性归结： (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),31,Horn子句归结与逻辑程序,PROLOG程序的运行是一种从问题语句(目标语句)开始的线性归结过程 每次归结时，子目标的选择顺序是从左到右，新子目标的插入顺序是插入子目标队列的左端，匹配子句的顺序是自上而下，搜索空子句的策略是深度优先，推理方式是反向推理，且有回溯机制 PROLOG程序的这种归结方法称为基于Horn子句SLD (Linear resolution with Selection function for Definite clause)归结，亦称为SLD反驳消解法,32,完！,