逻辑表示及归结系统.ppt

第6章 基于谓词逻辑的归结方法,一阶谓词逻辑概述 归结原理 归结反演系统 基于归结法的问题求解,定义：逻辑学是研究人类思维活动规律的科学. 方法：利用数学（符号化、公理化、形式化）的方法来研究这些规律. 作用：是表达人类思维和推理的最精确和成功的方法，成为 AI 的重要基础. 表现方式和人类自然语言非常接近 便于计算机做精确处理 分类：经典逻辑和非经典逻辑两大类，经典逻辑中命题逻辑和一阶谓词逻辑是基础.,1 一阶谓词逻辑概述,命题的定义：表示知识的陈述性形式或具有真假意义的陈述句. 例：A：张平是学生； B：树叶是绿色的； 命题的类型： 原子命题：表达单一意义、不能再分解. 如 P：天在下雨； Q: 天晴 复合命题：由连接词、标点和原子命题构成.如， P Q可表示：如果天在下雨则天不晴. 命题逻辑就是研究命题与命题之间关系的符号逻辑系统,包含语法、语义、演算等.,11 命题概念,原子命题是命题逻辑中最基本的单元,不能对其进行分解,也不能对其结构进行分析. 引发的问题: 限制了它的使用; 为了突破这种束缚, 发展了谓词逻辑. 原子命题可分解; 以命题中的谓词为基础进行分析研究.,1.2 谓词概念,原子命题分解为谓词、个体2部分。 例： 1、3是质数， x是质数， F(x)； 2、王二生于武汉市， x生于y， G(x,y)； 3、7=23， x=y z， H(x,y,z)； 3、王二、武汉市、7等，称为个体（具体）; 代表个体的变元，称为个体变元（抽象）； 刻画个体性质或个体之间关系的词叫谓词， 如 “是质数”、“生于”、“= ” 谓词中包含的个体数目称为谓词的元数. 在谓词P（x1，x2，xn）中,若每个xi都是个体常量、变元或函数，则称它为一阶谓词，若某个xi本身又是一个一阶谓词，则称它为二阶谓词,谓词与命题的区别更强的表达能力,1、有概括能力 例如，是一个城市，谓词 CITY（X） 2、可表示变化着的情况 命题值是恒真或恒假，谓词值可因参数而异 3、可在不同的知识之间建立高级联系 HUMAN（X）X是人，LAWED（X）X受法律约束，COMMIT（X）X犯法，PUNISHED（X）X受法律制裁 HUMAN（X）LAWED（X） 人人都要受法律约束 COMMIT（X）PUNISHED（X）犯罪，就要受惩罚 HUMAN（X）LAWED（X） COMMIT（X）PUNISHED（X）,2 归结原理,定理证明：已知一公式集 F1，F2，Fn，要证明一个公式 W 是否成立，即要证明 W 是公式集的逻辑推论. 方法： 直接法： F1F2FnW 是永真式. 间接法（反证法）： F1F2FnW为永假 基本思想：采用反证法将待证明的表达式转换为逻辑公式，然后再进行归结，归结能够顺利完成，则证明原定理是正确的.,2.1 归结原理概述,2.1 归结原理概述(续),理论依据: 空子句：一种没有任何解释能满足的子句，其取值总是假，简记为或NIL. 用归结法从子句集 S 导出的扩大子句集 S1(S归结式)，其不可满足性是不变的.(待证) 技术思路：设法检验原(或扩充的)子句集 S 是否含有空子句，若 S 集中存在空子句，则表明 S 为不可满足的. 过程: S S1 S2 Sn 归结过程可以一直进行下去，也就是要通过归结过程演绎出 S的不可满足性来，从而使定理得到证明.,几个概念,不含有任何连接词的命题(谓词)公式称为原子公式(原子). 原子或原子的否定统称为文字. 子句是由一些文字组成的析取式. 不包含任何文字的子句称为空子句.(不能用任何解释所满足) 子句构成的集合,称为子句集.,2.2 命题逻辑的归结法,1）归结式的定义及性质 归结：设 C1 与 C2是子句集中的任意两个子句，如果C1中的文字L1与C2中的文字L2互补，那么从C1和C2中分别消去L1和L2,并将两个子句中的余下部分析取，构成一个新的子句C，这一过程称为归结. C: C1 和 C2 的归结式; C1 和 C2: C 的亲本子句. 没有互补对的两子句没有归结式。,例设 C1=PQR, C2=Q S， C1中 L1=Q 与 C2 中 L2=Q互补. 得：C=PR S 例设 C1=P， C2=P P与P互补，可得：C= . 例设C1=PQ，C2=Q R，C3=P， 首先对 C1，C2 进行归结，得 C12=PR， 再对 C12，C3 归结，得 C123=R.,定理：两个子句 C1 和 C2 的归结式 C 是 C1 和 C2的逻辑结论.（即C1C2C） 证明: 设 C1=LC1， C2=（L）C2，通过归结可得到C= C1C2 因为 C1=L C1 = C1 L C1 L； C2= L C2LC2 C1C2 = ( C1L) (LC2) 由假言三段论得到： ( C1L) (LC2 ) ( C1C2 ) 而 C1C2 C1C2 = C C1C2 C 证毕,推论：子句集合S= C1，C2， Cn与S1= C， C1，C2， Cn的不可满足性是等价的（C是C1和C2的归结式，即S1是对S应用归结后得到的）. 证明： 设S是不可满足的，则C1 ，C2， Cn中必有一个为假，因而S1必为不可满足的. 设S1是不可满足的，则对于不满足S1的任一解释I，可能有两种情况： I使C为真，则C1，C2， Cn中必有一子句为假，因而S是不可满足的。 I使C为假，则根据定理有C1C2为假，即I或使C1为假，或使C2为假，因而S也是不可满足的。 由此, S和S1的不可满足性是等价的.,同理可证 Si 和 Si+1（Si导出的扩大的子句集）的不可满足性也是等价的，其中i=1，2，.,总结: 归结原理就是从子句集S出发，应用归结推理规则导出子句集S1 ，再从S1出发导出S2 ，依次类推，直到某一个子句集Sn出现空子句为止. 根据不可满足性等价原理，若已知Sn为不可满足的，则可逆向依次推得S必为不可满足的. 用归结法证明定理，只涉及归结推理规则的应用问题，过程比较简单，因而便于实现机器证明.,2）命题逻辑的归结过程,命题逻辑中，若给定公理集 F 和命题 P，则归结证明过程可归纳为： 把 F 转化为子句集表示，得子句集S0； 把命题 P 的否定式P也转化成子句集表示，并将其加到S0中，得S= S0P； 对子句集S反复应用归结推理规则，直到导出含有空子句的扩大子句集为止。即出现归结式为空子句的情况时，表明已找到了矛盾，证明过程结束.,例、设已知公理集为 P （1）； （PQ）R（2）； （ST）Q (3）； T （4）； 求证 R. 化成子句集表示后得 S=P，PQR，SQ，TQ，T，R 归结过程很简单，如右图的演绎树所示，由于根部出现了空子句，因此命题R得到证明.,PQR,PQ,Q,T,T,TQ,P,R,2.3 谓词逻辑中的归结原理,归结原理对子句集的基本要求(命题级): 无量词约束 子句只是文字的析取 否定符只作用于单个文字 子句间默认为合取 在谓词逻辑中，由于表达式中包含有变元,所以需要考虑变量的约束问题(作用范围): 1.谓词公式化子句集的方法. 2.在应用归结法时,先对公式作变量置换和合一等处理, 得到互补的基本式，然后才能进行归结.,新问题1: 量词问题? 谓词演算中,一般有两种形式: 前束范式和SKOLEM范式. 前束范式: 若一个谓词公式P的所有量词均非否定地出现在P的前部，且量词辖域是整个公式，称P为前束范式. 如 F (Q1x1)(Qnxn)M; (Qi:2值,M:析取式) SKOLEM范式:消去前束范式中的所有量词(方法如下)后所得到的谓词公式,也称SKOLEM标准型. : 若变量不受全称量词的约束(左边无),可用任意常量代替该变量; 否则, 用以其为因变量的函数代替该存在量词.,函数形式(几元函数)依赖于受几个全称量词约束. : 省略.,1）谓词公式的标准化,化子句集的方法,x P(x) yP(y) P(f(x,y) yQ(x,y) P(y) 1. 消蕴涵符 理论根据：a b = a b xP(x) yP(y) P(f(x,y) yQ(x,y) P(y) 2. 移动否定符 理论根据：(a b) = a b (a b) = a b (x)P(x)=(x)P(x) (x)P(x)=(x)P(x) x P(x) yP(y) P(f(x,y) y Q(x,y) P(y) = x P(x) yP(y) P(f(x,y) y Q(x,y) P(y),化子句集的方法（续1）,3.变量标准化 即：对于不同的量词约束，对应于不同的变量 方法: (x)A(x) (x)B(x) = (x)A(x) (y)B(y) x P(x) yP(y) P(f(x,y) w Q(x,w) P(w ) 4.量词左移 (保序前移到M的前部) 方法: (x)A(x)(y)B(y)=(x)(y)A(x)B(y) x y w P(x) P(y) P(f(x,y) Q(x,w) P(w),化子句集的方法（续2）,5. 消存在量词 (skolem化） 原则：对于一个受存在量词约束的变量，如果它不受全程量词约束，则该变量用一个常量代替，如果它受全程量词约束，则该变量用一个函数代替. x y w P(x) P(y) P(f(x, y) Q(x,w) P(w) = y P(a) P(y) P(f(a, y) Q(a, g（y）) P (g（y）),化子句集的方法（续3）,6. 化为合取范式 即(ab) (cd) (ef)的形式 方法: P(x) Q(x) R(x) P(x) Q(x) P(x) R(x) P(x)Q(x)R(x)P(x)Q(x) R(x)P(x)Q(x)R(x) P(x)Q(x)R(x)P(x)Q(x)R(x)P(x)Q(x)R(x) y P(a) P(y) P(f(a, y) Q(a,g（y）) P(g（y）) = y P(a) P(y) P(f(a,y) P(a) Q(a, g（y）) P(a) P(g（y）),化子句集的方法（续4）,7. 隐去全程量词 P(a) P(y) P(f(a,y) P(a) Q(a, g（y）) P(a) P(g（y）) 8.表示为子句集: 以逗号替代所有的合取符号 P(a) P(y) P(f(a,y)，P(a) Q(a, g（y）)，P(a) P(g（y）) 9. 变量标准化（变量换名） 即：不同的子句，使用不同的变量 P(a) P(y1) P(f(a,y1)，P(a) Q(a, g（y2）)，P(a) P(g（y3）),课堂小练习: 化下列公式成子句形式,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） ,2) 置换和合一,问题2: 表达式是否相同或匹配? P(x) Q(y）与 P(a) R(z） 思路: 个体变量的替换. 方法: 置换和合一 置换: 在谓词公式中用项(常,变,函数)替换变量, 形如: s= t1/v1 , t2/v2 , , tn/vn 对公式 E 实施置换 s 后得到的公式称为 E 的例，记作 Es. 例：s1= z/x , A/y , 则： P x, f(y), B s = P z, f(A), B ,2) 置换和合一(续1),合成置换: 有时需对表达式进行多次置换，如用s1、 s2依次进行置换（即（E s1）s2），这时可以把两个置换合成为一个置换（记为s1 s2）. 合成置换是由两部分组成的：一部分仍是s1的置换对，只是s1中的项被s2作了置换；另一部分是s2中与s1不同的那些变量对。例如： s1= g(x,y)/z , s2= A/x, B/y, C/w, D/z s1s2= g(A,B)/z , A/x, B/y, C/w 性质: （E s1）s2=E（s1s2），(结合律) 但一般情况下置换是不可交换的，即s1s2 s2s1。 s2s1=A/x,B/y,C/w, D/z s1s2,2) 置换和合一(续2),合一就是通过项对变量的置换,而使表达式(文字)一致. 若存在一个置换 s 使得表达式集Ei中每一个元素经置换后的例有：E1s =E2s= E3s=，则称表达式集Ei是可合一的，这个置换 s 称作Ei的合一者. 例.P（x，f（y），B），P（x, f（B）,B） s=A/x，B/y，得 P（A，f（B），B） .,2) 置换和合一(续3),如果 g 是公式集Ei的一个合一者,如果对Ei的任意一个合一者s都存在一个置换s，使得s=gs，则称g为表达式Ei的最简单合一者mgu. 例.P（x，f（y），B），P（x，f（B），B） g=B/y为该式的mgu. 因为s=A/x，B/y， 置换s =A/x,使s=gs.,求最简单合一者的算法: 1. 令 W= F1, F2; /输入 2. k=0, W0=W, g0= ;/循环次数,公式集合,置换的初始化 3. 如果 Wk 已合一,停止, gk=mgu; /成功退出 否则, 找不一致集 Dk; 4.若 Dk中存在元素vk和tk,其中vk不出现于tk中,转(5), 否则,不可合一; /失败退出 5. 令gk+1 = gktk/ vk, Wk+1 = Wk tk/ vk, / 置换合成, 公式集合变换 6. k=k+1 转(3),2) 置换和合一(续4),例: S= P(a,x,h(g(z), P(z,h(y),h(y) 1. g0=; Sg0不是单元素集,故求不一致集D0=a,z; 2. g1=g0a/z; Sg1=P(a,x,h(g(a), P(a,h(y),h(y)不是单元素集,故D1=x, h(y); 3. g2=g1h(y)/x; Sg2=(Sg1)h(y)/x =P(a, h(y),h(g(a), P(a,h(y),h(y)不是单元素集,故D2=g(a), y; 4. g3=g2g(a)/y; Sg3=(Sg2)g(a)/y= P(a,h(g(a),h(g(a), P(a,h(g(a),h(g(a) 是可合一的. 即 g3=a/zh(y)/xg(a)/y= a/z,h(y)/xg(a)/y= a/z,h(g(a)/x,g(a)/y 是一个mgu.,3) 谓词逻辑中的归结式,归结式: 对于子句 C1L1 和 C2L2，如果L1 与 L2 可合一，且 s 是其合一者，则(C1C2)s 是其归结式. 例： P(x)Q(y), P(f(z)R(z) = Q(y)R(z) (s=f(z)/x) 选不同文字对做归结时,可得不同的归结式 练习: C1= P(x，f(y) Q(y) C2= P(z，f（A）) Q(z),3) 谓词逻辑中的归结式(续),注意点: 被归结的子句 C1, C2 应具有不同的变量. 方法:变量换名 在求归结式时,不能同时消去两个互补文字对,消去两个互补文字对所得到的结果不是亲本子句的逻辑推论. 例.C1= P() Q(), C2 = P() Q() 如在参加归结的子句内含有可合一的文字,则应先对这些文字进行合一,化简后再归结. 例. C1= P(x) P(f(a) Q(x), C2 = P(y) R(b),定义谓词 写出已知条件和结论的谓词关系公式 化为 Skolem 标准型 求子句集合 S 对 S 中可归结的子句做归结(置换和合一) 归结式仍放入S中,反复归结过程 看能否导出空子句,4) 谓词逻辑中的归结过程,例、已知：1.会朗读的动物是识字的；2.海豚都是不识字的；3.有些海豚很机灵。 证明：有些很机灵的动物不会朗读。 已知：1.(x)(R(x)L(x); 2.(x)(D(x) L(x); 3.(x)(D(x)I(x) 求证：(x)(I(x) R (x) 化简前提条件公式，结论取反，得子句集： （1）R(x) L(x) （2）D(y) L(y) （3a）D（A） （3b）I（A） （4）I(z) R (z),A,/,z,A,/,x,A,/,y,（1）R(x) L(x) （2）D(y) L(y) （3a）D（A） （3b）I（A） （4）I(z) R (z) 从子句集求归结式，并将它加进子句集，连续进行直到产生空子句为止，上图的归结过程代表一个可行的证明过程,归结反演树,3 归结反演系统 3.1 产生式系统的基本算法,综合数据库：子句集 (子句间为合取关系) 规则集合：IF cx（Si）和 cy（Si）有归结式rxy THEN Si+1=Sirxy 目标条件：Sn中出现空子句 过程 1 Clauses：= S；S为初始的基本子句集。 2 until NIL 是 Clauses 的元素，do： 3 begin 4 在 Clauses 中选两个不同的可归结的子句ci 、cj 5 求 ci 、cj 的归结式rij； 6 Clauses：= rij Clauses 7 end；,3.2 搜索策略,任务:是在算法的第4步中确定选哪两个子句做归结，以及在第5步决定这两个子句中对哪一个文字做归结 主要策略: 宽度优先: 第一级(基本集)第二级 支持集: 归结时，至少选一个是与目标公式否定式(本身或后裔)有关的子句. 单元子句优先: 至少有一个是单文字子句 线性输入形: 至少有一个是从基本子句集中挑选 祖先过滤形: 有一个母子句或者从基本集中挑选，或者从该母子句的先辈子句中挑选,4 基于归结法的问题解答系统,4.1 提取回答的方法 例、if Fido goes wherever John goes and if John is at school, where is Fido? 分析: 两个已知事实和一个询问. 思路: 从事实出发演绎得到询问的答案. 步骤: 1. 先用谓词公式表示问题： 前提：(x)( AT(John, x) AT(Fido, x) ); AT(John, School) 目标：(x) AT(Fido, x) 子句集: AT(John, x1) AT(Fido, x1), AT(John, School), AT(Fido, x2),2.证明目标公式是前提公式集的逻辑推论 3.找出一个x的例，来回答Fido 在何处的询问. 关键：把询问表达为一个有存在量词约束的目标公式.,归结反演树,修改证明树,AT(John, x1) AT(Fido, x1),x2/x1,AT(John, School),School/x2,AT(Fido, x2) AT(Fido, x2),AT(John, x2) AT(Fido, x2),AT(Fido, School),例: 在天花板上吊有一串香蕉的房间里，有一个可移动的箱子，问一只猴子如何规划自己的行动使得它能摘到香蕉.,c,a,问题描述: 初始状态为 S0： ONBOX ，AT（box，b）， AT（Monkey，a）， HB 目标状态为 HB. 谓词的含义： 1. 当猴子在箱顶上时，ONBOX 取真； 2. 当猴子拿到香蕉时，HB 取真； 3. 谓词 AT（y，x）当 y 处于 x 位置时取真。 猴子的行为用4个规则表示，每条规则的描述形式均用谓词演算的公式组表示. P:前提条件，D:规则应用后，应从状态中删去部分，A: 添加部分的状态.,goto(u) P: ONBOX(x) AT（Monkey，x） D: AT（Monkey，x） A: AT（Monkey，u） Pushbox(v) P: ONBOX(x)AT（Monkey，x）AT（box，x） D: AT（Monkey，x）, AT（box，x） A: AT（Monkey，v）, AT（box，v） Climbbox P: ONBOX(x)AT（Monkey，x）AT（box，x） D: ONBOX A: ONBOX Grasp P: ONBOXAT（box