第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）),