week8-北航6系人工智能课件.ppt

1、北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 1第第 三三 章章 基于逻辑的问题求解方法基于逻辑的问题求解方法第 8 周 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 2认知区域认知区域 功能功能 研究学派研究学派- -10s: 目标实现1s: 简单操作合成100ms:初级熟练操作10ms: 符号存取理性带理性带认知带认知带神经带神经带逻辑学派、知逻辑学派、知识工程学派识工程学派认知学派认知学派（代表作：（代表作：- SOAR）联结学派联结学派认知学派的层次划分认知学派的层次划分北京航空航天

2、大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 3基于逻辑的问题求解方法基于逻辑的问题求解方法n逻辑是人工智能的重要基础逻辑是人工智能的重要基础n一阶逻辑的基本概念回一阶逻辑的基本概念回顾顾n基于一阶逻辑的演绎推理技术基于一阶逻辑的演绎推理技术 n应用逻辑系统应用逻辑系统北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 4逻辑是人工智能的重要基础逻辑是人工智能的重要基础n人工智能遵循人工智能遵循符号原理符号原理：将所有与问题有关的对象、对象、关系以及概念关系以及概念等进行形式化的表示形式化的表示和处理处理。n

3、 一阶一阶逻辑满足形式化表达和处理要求逻辑满足形式化表达和处理要求 ：w 类自然语言的形式化的符号语言类自然语言的形式化的符号语言 （谓词公式描述谓词公式描述）w 强有力的推理方法（强有力的推理方法（公理化推理方法、归结法公理化推理方法、归结法）；）；w 坚实的理论证明基础（坚实的理论证明基础（语义模型、推理的可靠性、语义模型、推理的可靠性、完备性研究完备性研究等等）。 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 5逻辑是人工智能的重要基础逻辑是人工智能的重要基础n 一阶逻辑一阶逻辑对对AI的贡献的贡献：w 提出了提出了陈述性陈述性知识表示

4、方式知识表示方式 ；w 将将知识描述与知识处理相分离知识描述与知识处理相分离；w 基于基于一阶逻辑扩展了多种应用逻辑一阶逻辑扩展了多种应用逻辑- 如如时序时序 ( p53 )、模糊、非单调、模糊、非单调等多种等多种应用逻辑应用逻辑。北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 6基于逻辑的问题求解方法基于逻辑的问题求解方法n逻辑是人工智能的重要基础逻辑是人工智能的重要基础n一阶逻辑的基本概念回一阶逻辑的基本概念回顾顾n演绎推理技术演绎推理技术 n应用逻辑系统应用逻辑系统北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家

5、重点实验室 Slide 7u 字符表字符表一阶逻辑的基本概念回一阶逻辑的基本概念回顾顾一阶谓词逻辑知识表示方法一阶谓词逻辑知识表示方法w 项、合式谓词公式项、合式谓词公式w 演绎推理方法演绎推理方法w 解释与赋值解释与赋值北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 8一阶谓词逻辑的符号体系一阶谓词逻辑的符号体系 - - 字符表字符表n常元常元: :n变元变元: :n函数函数( (词词) )符符: :n谓词符谓词符: :n逻辑联词逻辑联词: :n量词量词: :n其它其它: :a, b, c,.; A, B, C,.; x, y, z,.;Fn

6、, gm, .; e.g., f1(x): x的父亲。的父亲。Pn, Qm, R, .; e.g., brother2(x, y)。 , , , , 。 , 。 (, ), ，。北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 9一阶逻辑的基本概念回一阶逻辑的基本概念回顾顾n一阶谓词逻辑的符号体系一阶谓词逻辑的符号体系w 字符表字符表w 项、谓词合式公式项、谓词合式公式w 等价公式等价公式w 演绎推理方法演绎推理方法北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 10项、谓词合式公式项、谓词合式公

7、式n 项：项：常元常元: a,b,; 变元变元: x,y,.;函词函词: fn(x1,x2,xn) ，其中，其中， xi是项。是项。n 合适谓词公式合适谓词公式原子公式原子公式 Pn(x1,x2,xn)是合式谓词公式是合式谓词公式，其中，其中， xi 是项。是项。设设: A,B: A,B是合式谓词公式，则是合式谓词公式，则 A A，A A B B，A AB B，A AB, B, ( x) A A 是合式谓词公式。是合式谓词公式。 例：例：( x) ( P(x) ( y) (R(y) S(x,y) ) )北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Sli

8、de 11等价公式等价公式n等价公式( p41-42 )( p41-42 )得摩根定律得摩根定律： (P Q) P Q (P Q) P Q 分配律：分配律： R ( P Q ) （R P ） ( R Q ) R ( P Q ) （R P） ( R Q )蕴含等价式：蕴含等价式： P Q P Q .；量词转换律量词转换律: ( x)P(x) ( x) P(x) ( x)P(x) ( x) P(x) 全称量词消去规则：全称量词消去规则： （ x)P(x) P(y) 存在量词消去规则：存在量词消去规则：（ x)P(x) P(c) c为常元为常元.。北京航空航天大学软件开发环境国家重点实验室北京航空航

9、天大学软件开发环境国家重点实验室 Slide 12演绎推理演绎推理演绎推理方法演绎推理方法推理：推理：根据一定准则，由前提判断导出称为结论的思维过程。根据一定准则，由前提判断导出称为结论的思维过程。演绎推理演绎推理、归纳推理、类比推理、归纳推理、类比推理推理方式：推理方式：A1,A2,An |= B, iff （ x）（）（ P(x) Q(x) ） P(a) - Q(a) ，推理规则推理规则：推理过程：推理过程：反复运用反复运用等价公式等价公式、推理规则推理规则对已对已知的谓词公式进行变换，得到所需的逻辑结论的知的谓词公式进行变换，得到所需的逻辑结论的过程。过程。归归 原原理理 结结北京航空航

10、天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 13解释与赋值解释与赋值n解释定义:一个解释 I 由以下四部分组成。w（1）指定一个非空集合 DI，称为 I 的论域；w（2）对于每个常元 a，指定 DI 中的一个元素 aI；w（3）对于每个n元函数符号 f，指定DI上的一个n元运算符 fIw（4）对于每个n元谓词符号 P，指定DI上的一个 n 元谓词 PI北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 14解释与赋值解释与赋值n 赋值定义:w设 I 是一个解释，将所有变元变元组成的集合映射到论域 DI 的

11、函数称为 I 中的赋值v。n 解释和赋值共同规定了项和公式的意义。n 例：设 DI 为自然数集合，fI 是自然数乘法，gI 是自然数加法，aI = 2，I中赋值 v 使 v(x) = 1。 项 f(g(a,x),af(g(a,x),a) )在 I 和 v 下的意义： I（f(g(a,x),af(g(a,x),a) )）(v) = ?北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 15基于逻辑的问题求解方法基于逻辑的问题求解方法n逻辑是人工智能的重要基础逻辑是人工智能的重要基础n一阶逻辑的基本概念回一阶逻辑的基本概念回顾顾n 机器演绎推理技术机器

12、演绎推理技术 n 应用逻辑系统应用逻辑系统北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 16机器演绎推理技术机器演绎推理技术 归结法归结法n 谓词公式的规范化谓词公式的规范化w 谓词公式的合取范式谓词公式的合取范式w 合取范式的子句集形式合取范式的子句集形式n 推理过程规范化推理过程规范化w 命题逻辑归结原理命题逻辑归结原理w 变量置换与合一变量置换与合一w谓词谓词归结证明系统的相关技术归结证明系统的相关技术北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 17谓词公式的谓词公式的子句形式子句形

13、式n文字：文字：n子句：子句：n空子句：空子句：n基子句：基子句：子句与合适子句与合适公式公式对应关系对应关系原子公式及其否定：原子公式及其否定： P(x1,x2,xn) ， Q(x1,x2,xm) 文字的有穷集合：文字的有穷集合： P(x1,x2,xn) ， Q(x1,x2,xm）不含任何变元的子句：不含任何变元的子句：P(A), R(b, f(b)不含任何文字的子句：不含任何文字的子句：空子句空子句 永假公式永假公式 F F非空子句非空子句 L1, L2, , Ln 析取式析取式 L1 L2 Ln子句集子句集S SA A=A1, A2, An 无无 型前束合取范式型前束合取范式北京航空航天

14、大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 18子句的子句的标准范式标准范式n无无 型前束合取范式型前束合取范式:（Q1x1）(Q2x2）（Qnxn）M 其中， Qi：全称量词；：全称量词； xi：变元：变元母式：母式：M = (A11 A12 A1n ) (Am1 Am2 Aml ) 是是合取范式合取范式， 其中其中, Aij是文字。是文字。子句集：子句集： S = A A1111 A A12 12 A A1n 1n ， A Am1m1 A Am2 m2 A Amlml 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实

15、验室 Slide 19n合式谓词公式化子句集步骤合式谓词公式化子句集步骤 ( p43 )( p43 )子句的子句的标准范式标准范式 合式公式合式公式 A 变换成子句集变换成子句集 SA 实例实例： A=( x) ( P(x) ( y) (R(y) S(x,y) ) )北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 20合式公式化子句集实例合式公式化子句集实例nA A (x)(P(x) (y)(R(y) S(x,y) (x)(P(x) (y)( R(y) S(x,y) 消 (x) (y)(P(x) ( R(y) S(x,y) 前束 (x) (P(

16、x) ( R(f(x) S(x, f(x)消 子句集子句集: :SA = P(x), R(f(x) S(x, f(x) 前束前束 (子句子句1 , 1 , 子句子句2)2)母母 式式北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 21习题：将谓词公式化为子句形式习题：将谓词公式化为子句形式n ( x)P(x) ( x ) P(x) n ( x)(P(x) ( ( y)(P(y) P(f(x,y) ( y)(Q(x,y) P(y)北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 22机器演绎推理技术

17、机器演绎推理技术 归结法归结法n 谓词公式的规范化表示谓词公式的规范化表示w 谓词公式的合取范式谓词公式的合取范式w 合取范式的子句集形式合取范式的子句集形式n 推理过程规范化推理过程规范化w 命题逻辑归结原理命题逻辑归结原理w 变量的变量的置换置换与与合一合一概念概念w 谓词谓词归结证明系统的相关技术归结证明系统的相关技术北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 23n 核心思想核心思想：w要证要证 B B = = A A1 1，A A2 2 ， A An n |= w语义证明方法语义证明方法1： |= A A1 1 A A2 2 A

18、An n w语义证明方法语义证明方法2： A A = = A A1 1 A A2 2 A An n |= F命题逻辑归结原理命题逻辑归结原理n 支撑定理支撑定理：设设 SA 是合式谓词公式是合式谓词公式 A 的的标准型子句集标准型子句集，则，则 A 为永为永假的充要条件是假的充要条件是 SA 不可满足。不可满足。( 证明证明 SA不可满足）不可满足）即：即：SA = SB |= 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 24命题逻辑归结原理命题逻辑归结原理n归结定义：归结定义：设设C C1 1,C,C2 2是任意的两个命题子句，其中，是任

19、意的两个命题子句，其中， C C1 1 = L= L1 1 C C1 1 , C , C2 2 = L= L2 2 C C2 2 ，L L1, 1, L L2 2是互补原是互补原子命题，即子命题，即 L L1 1 = = L L2 2。那么，分别从。那么，分别从 C C1 1 和和 C C2 2 中删去中删去 L L1 1 和和 L L2 2，将其余部分组成的一个新的析，将其余部分组成的一个新的析取式取式 C C = = C C1 1 C C2 2 称为称为 C C1 1 和和 C C2 2 的归结式。的归结式。北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验

20、室 Slide 25命题逻辑归结原理命题逻辑归结原理n归结定义应用例归结定义应用例: : P Q R R T PP P R R P P Q T不可归结不可归结 P R P Q北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 26命题逻辑归结原理命题逻辑归结原理v 定理：定理：子句子句 C C1 1 和和 C C2 2 的归结式的归结式 C C 是是 C C1 1 和和 C C2 2 的的逻辑推论逻辑推论，即，即， C C1 1, C, C2 2 |= |= C C 。v 推论：推论：设设 C C 是是 C C1 1 和和 C C2 2 的归结式，

21、则子句集的归结式，则子句集 S = S = C C1 1，C C2 2 ， C Cn n 与与子句集子句集 S1 = S1 = C C，C C1 1，C C2 2 ， C Cn n 的的不可满足性不可满足性等价。等价。归结式性质：归结式性质：C = L1 C = L1 C1C1， L2 L2 C2 C2 = C1 C1 C2C2北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 27命题逻辑归结原理命题逻辑归结原理n命题归结算法：命题归结算法：w 将已知前提公式集将已知前提公式集 A A 化为子句集化为子句集 SA；w 把待证命题把待证命题 的否定

22、式的否定式 化为子句集，并将其化为子句集，并将其加入到前提子句集加入到前提子句集 SA 中，获中，获子句集子句集 S0 = SA ；w 对子句集对子句集 Si（i = 0, 1, , n), 应用归结推理规则应用归结推理规则，获，获 Si+1 = C Si, 重复此过程，直至推出包含重复此过程，直至推出包含空子句空子句的扩大子句集的扩大子句集 Sn 为止。为止。北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 28命题逻辑归结原理应用实例命题逻辑归结原理应用实例A = A = P, (P Q) R, (S T) Q, T |= R S0= P,

23、P Q R, S Q , T Q, T, R |= P Q R R P Q P Q T Q T T 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 29问题：问题：n命题归结：命题归结：C1 = PC2 = Pn谓词归结：谓词归结：C1 = P(f(a)C2 = P(x)?需解决谓词中需解决谓词中变量的变量的置换置换与与合一合一问题问题！北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 30n 谓词公式的规范化表示谓词公式的规范化表示w 谓词公式的子句形式谓词公式的子句形式w 子句的标准范式子句的

24、标准范式n 推理过程规范化推理过程规范化w 命题逻辑命题逻辑归结原理归结原理w 谓词公式谓词公式变量变量的的置换置换与与合一合一概念概念w 谓词谓词归结证明系统的相关技术归结证明系统的相关技术机器演绎推理技术机器演绎推理技术 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 31谓词公式谓词公式变量的置换变量的置换与合一与合一n置换置换及其及其实例：实例：w设设 E E 为任一为任一简单表达式，简单表达式，x x1 1,x,x2 2, ,x,xn n为为 E E 中的不同中的不同变量，变量，t t1 1,t,t2 2, ,t,tn n 为为项项，

25、则，则: :集合集合 S = S = t t1 1/x/x1 1, t, t2 2/x/x2 2, , t, tn n/x/xn n 为一为一置换置换ES = E ES = E t1,t2,t1,t2,tn,tn 为为 用用 t ti i（i=1,2,i=1,2,n,n）处处处处替换替换表达式表达式 E E 中出现的变元中出现的变元 x xi i（i=1,2,i=1,2,n n）得到）得到的一个的一个实例实例。x1,xx1,x2 2, ,xn,xn北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 32谓词公式谓词公式变量的置换变量的置换与合一与合

26、一n 例：设表达式例：设表达式 E = P(x, f(y), B)E = P(x, f(y), B) 置换置换 实例实例 - -S1= z/x, w/yz/x, w/yS2= g(z)/x, A/yz)/x, A/yS3= C/x, A/y/x, A/yES1= P(z, f(w), B)ES2= P(g(z), f(A), B)ES3= P(C, f(A), B)北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 33谓词公式中谓词公式中变量的置换变量的置换与与合一合一n置换的合成：置换的合成：设两个设两个置换置换分别为分别为 = = t t1

27、1/u/u1 1, t, t2 2/u/u2 2, , t, tm m/u/um m , = tt1 1/v/v1 1, t, t2 2/v/v2 2, , t, tn n/v/vn n , 与与 的合成的合成: = t t1 1 /u/u1 1, t, t2 2 /u/u2 2, ,t,tm m /u/um m，tt1 1/v/v1 1, , tt2 2/v/v2 2, ,t,tn n/v/vn n （v vi i u ui i) )。置换过程如下：置换过程如下： 首先，利用首先，利用 中的置换对对变量中的置换对对变量 u u1 1,u,u2 2, ,u,um m 进行置进行置换；如果置换后

28、的项中出现换；如果置换后的项中出现 v vi i（i=1,2,i=1,2,n n）, ,再用再用 中中的置换对的置换对 v vi i 进行进行进一步的进一步的置换。置换。 而后，用而后，用 的置换对对变量的置换对对变量 v v1 1,v,v2 2, ,v,vn n进行置换进行置换，其中，其中，vivi ujuj 。北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 34谓词公式中变量的谓词公式中变量的置换置换与与合一合一n置换合成置换合成的运用的运用实例：实例： 设设 s s1 1= g(x,y)/z , s= g(x,y)/z , s2 2= A

29、/x,B/y,C/w,D/z = A/x,B/y,C/w,D/z 置换置换合成性质合成性质：满足结合律结合律: (s s1 1 s s2 2)s)s3 3 = s= s1 1(s(s2 2s s3 3) ) 不满足交换律交换律: (s s1 1 s s2 2) ) (s (s2 2 s s1 1) )s s1 1 s s2 2 = = g(A,B)/z, A/x,B/y,C/w g(A,B)/z, A/x,B/y,C/w 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 35变量的变量的置换与置换与合一合一n表达式的表达式的可合一性可合一性与与合

30、一者合一者：设有表达式集设有表达式集 E = E = E Ei i 和置换和置换 S S。如果。如果 S S 对对 E E 中所有中所有表达式进行置换后得到的实例满足表达式进行置换后得到的实例满足 E E1 1S = S = E E1 1S = .= S = .= E En nS S，则称表达式集，则称表达式集 E Ei i 是可合一的，是可合一的，S S为为 E Ei i 的合一者的合一者 例：例：设表达式集 Ei = P(x, f(y), B)，P(x, f(B), B) 置换1： s1 = A/x, B/y 置换后有：E1s1 = E2s1 = P( A,f(B),B )置换2： s2

31、= B/y 置换后有：E1s2 = E2s2 = P( x,f(B),B )北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 36变量的变量的置换与置换与合一合一 最一般合一者最一般合一者（mgu Most General Unifier） 是表达式是表达式EEi i 的最一般的合一者，如果它满足以下关系的最一般的合一者，如果它满足以下关系：对于表达式集：对于表达式集 EEi i 的任一合一者的任一合一者 S S，都存在另一个置，都存在另一个置换换 SS，使得，使得 S = S = S S，或者，或者 ES = ( EES = ( E )S )S

32、 成立。成立。 例： 设 s = A/x, B/y = = B/y ，S = S = A/x, 有：S S = = S S 。北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 37演绎推理技术演绎推理技术n 谓词公式的规范化表示谓词公式的规范化表示w 谓词公式的子句形式谓词公式的子句形式w 子句的标准范式子句的标准范式n 推理过程规范化推理过程规范化w 命题逻辑命题逻辑归结原理归结原理w 谓词公式谓词公式变量变量的的置换置换与与合一合一概念概念w 谓词谓词归结证明系统的相关技术归结证明系统的相关技术北京航空航天大学软件开发环境国家重点实验室北京航

33、空航天大学软件开发环境国家重点实验室 Slide 38谓词谓词归结归结证明证明系统的相关技术系统的相关技术 合一匹配算法合一匹配算法 一阶谓词归结原理一阶谓词归结原理 归结证明系统的基本推理算法归结证明系统的基本推理算法 归结证明系统的推理策略归结证明系统的推理策略北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 39合一匹配算法：合一匹配算法：用形式化的方法，用形式化的方法，寻找两个子句的寻找两个子句的最一最一般合一者，般合一者，构成该子句对的构成该子句对的互补文字。互补文字。北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环

34、境国家重点实验室 Slide 40合一匹配算法：合一匹配算法：n分歧集定义：分歧集定义：w 设设 EiEi 是简单表达式的非空集合，将是简单表达式的非空集合，将 EiEi 的所的所有元素从左自右扫描，如果找到对应符号串中第一个不相有元素从左自右扫描，如果找到对应符号串中第一个不相同的符号，则称以此符号位置为起点的子表达式构成的集同的符号，则称以此符号位置为起点的子表达式构成的集合为合为 EiEi 的一个分歧集。的一个分歧集。例：例： 设设 E Ei i= P(f(x),h(y),a= P(f(x),h(y),a), P(f(x),z,a), P(f(x),h(y),b), P(f(x),z,a

35、), P(f(x),h(y),b)EEi i 的分歧集：的分歧集： h(y),z h(y),z ； a a, b b 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 41赋初值：赋初值： E Ei i = E E1 1， E E2 2 k = 0, k = = E E1k 1k k E E2k 2k k 求置换实例求置换实例 E Ei i k k 的分歧集的分歧集D k k+1 = k t/x , k = k + 1输出输出 = mgu k输出输出 E Ei i 不可合一不可合一yesNo( x)( t)(x D k t D k ）yesNoE

36、 Ei i : 表达式；表达式；k: 计数器；计数器； : 置换空集置换空集k: 第第k次求得的最一般合一者次求得的最一般合一者(mgu)Dk:第第k次求得的分歧集。次求得的分歧集。合一匹配算法：合一匹配算法：北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 42n例1: 设设EiEi=P(f(a),g(x),P(y,y)=P(f(a),g(x),P(y,y)w 置换置换 0 = 0 = = = ; ; 分歧集分歧集 D0 = f(a), y D0 = f(a), y w 置换合成置换合成 1 = 1 = f(a)/y f(a)/y w 实例实例

37、EiEi 1 1 = P(f(a),g(x),P(f(a),f(a)= P(f(a),g(x),P(f(a),f(a)w 分歧集分歧集 D1 = D1 = g(x)g(x), , f(a)f(a) w 打印打印“EiEi 不可合一不可合一”。合一匹配算法应用实例：合一匹配算法应用实例：北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 43合一匹配算法应用习题：合一匹配算法应用习题：2 2、设设EiEi=P(a,x,h(g(z),P(z,h(y),h(y)=P(a,x,h(g(z),P(z,h(y),h(y) 对对EiEi 实施合一匹配算法。实施合

38、一匹配算法。1、判断下列文字能否合一，若不能，请说明理由，、判断下列文字能否合一，若不能，请说明理由，若能，请求出其若能，请求出其mgu 。 EiEi=P(f(x,g(z),h(A),P(f(x,y),z)=P(f(x,g(z),h(A),P(f(x,y),z)北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 44谓词谓词归结证明系统的相关技术归结证明系统的相关技术 合一匹配算法合一匹配算法 一阶谓词归结原理一阶谓词归结原理 归结证明系统的基本推理算法归结证明系统的基本推理算法 归结证明系统的推理策略归结证明系统的推理策略北京航空航天大学软件开发

39、环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 45一阶谓词归结原理一阶谓词归结原理n归结定义：归结定义：设设C C1 1,C,C2 2是任意的两个是任意的两个谓词谓词子句子句，其中，其中， C C1 1 = L= L1 1 C C1 1 , C, C2 2 = L= L2 2 C C2 2 ，L L1, 1, L L2 2是是可化为可化为互补文互补文字的两个原子谓词公式字的两个原子谓词公式, ,（即二者间存在最一般合一者（即二者间存在最一般合一者mgu ）。那么，）。那么，C C1 1 和和 C C2 2 的归结式的归结式 C C 可由下式求得可由下式求得：C C=

40、 = C C1 1-L L1 1 C C2 2-L L2 2 = = C C1 1 C C2 2 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 46一阶谓词归结原理演算实例一阶谓词归结原理演算实例P(x) P(x) Q(x)Q(x) = = P(x, f(y) Q(x) R(f(a), y) P(f(f(a),z) R(z,w)Q(f(f(a) R(f(a), y) R(f(y),w) = f(f(a)/x, f(y)/z北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 47谓词谓词归结证明系统

41、的相关技术归结证明系统的相关技术 合一匹配算法合一匹配算法 一阶谓词归结原理一阶谓词归结原理 归结证明系统的基本算法归结证明系统的基本算法 归结证明系统的推理策略归结证明系统的推理策略北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 48设公式集设公式集 S S 和待证目标公式和待证目标公式 W W， 将公式集将公式集 S, S, W W 化成子句集化成子句集 S S0 0； CLAUSESCLAUSES = = S S0 0 ； UntilUntil CLAUSES CLAUSES, do:, do: beginbegin 从从 CLAUSES

42、CLAUSES中中选择选择两个不同的两个不同的可归结子句可归结子句 C C1 1和和 C C2 2； 对对 C C1 1 和和 C C2 2 中互反文字进行归结，获归结式中互反文字进行归结，获归结式 C C，且，且 CLAUSES = CLAUSES CLAUSES = CLAUSES C C ； endend一阶谓词归结证明系统的基本算法一阶谓词归结证明系统的基本算法北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 49一阶谓词归结一阶谓词归结证明系统证明系统应用实例（应用实例（1 1）已知：已知：w 会朗读的人是识字的人，会朗读的人是识字的人

43、，w 海豚都不识字，海豚都不识字，w 有些海豚很机灵。有些海豚很机灵。求证求证: :w有些很机灵的东西不会朗读有些很机灵的东西不会朗读一阶谓词描述：一阶谓词描述：w( ( x)(R(x) )(R(x) L(x) L(x)w( ( x)(D(x) )(D(x) L(x) L(x)w( ( x)(D(x) )(D(x) I(x) I(x)求证：求证： w =( ( x)(I(x) )(I(x) R(x) R(x)设原子谓词公式：设原子谓词公式：R(x)R(x)：x x 会朗读；会朗读； L(x)L(x)：x x 识字识字 D(x)D(x)：x x 是海豚；是海豚； I(x)I(x)：x x 机灵机

44、灵W = ( ( x)(I(x) )(I(x) R(x) R(x) = ( x) (I(x) (I(x) R(x) R(x) = ( x) I(z) R(z)北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 50一阶谓词归结一阶谓词归结证明系统证明系统应用实例应用实例（2 2）子句集：子句集： S S0 0 = = R(x)R(x) L(x), L(x), D(y)D(y) L(y), D(A), I(A), L(y), D(A), I(A), I(z)I(z) R(z)R(z) 求证：求证： S S0 0 |=|= 北京航空航天大学软件开发环境

45、国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 51一阶谓词归结证明系统一阶谓词归结证明系统应用实例应用实例（3 3）S S0 0 = = R(x)R(x) L(x), L(x), D(y)D(y) L(y), L(y), D(A), D(A), I(A), I(A), I(z)I(z) R(z)R(z) A/yA/zA/x D(y)D(y) L(y)L(y)D(A)D(A) I(z)I(z) R(z)R(z)I(A)I(A) R(x)R(x) L(x)L(x) L(A)L(A) 空空 L(A)L(A)R(A)R(A)北京航空航天大学软件开发环境国家重点实验室北京航空航天

46、大学软件开发环境国家重点实验室 Slide 52谓词谓词归结证明系统的相关技术归结证明系统的相关技术 合一匹配算法合一匹配算法 一阶谓词归结原理一阶谓词归结原理 归结反演系统的基本算法归结反演系统的基本算法 归结证明系统的推理策略归结证明系统的推理策略北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 53归结证明系统的归结证明系统的推理策略推理策略n搜索策略的搜索策略的完备性完备性如果给定问题的子句集存在矛盾，便可以通过运用如果给定问题的子句集存在矛盾，便可以通过运用某种归结搜索策略某种归结搜索策略, ,最终构造出一棵以最终构造出一棵以 结尾的结

47、尾的归结反演树，称此归结搜索策略是完备的。归结反演树，称此归结搜索策略是完备的。n 策略的策略的搜索效率搜索效率需要兼顾策略的完备性和高效性。需要兼顾策略的完备性和高效性。n 常用归结搜索策略常用归结搜索策略北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 54推理策略推理策略实例（实例（1 1）已知：已知：w 会朗读的人是识字的人，会朗读的人是识字的人，w 海豚都不识字，海豚都不识字，w 有些海豚很机灵。有些海豚很机灵。设原子谓词公式：设原子谓词公式： R(x)R(x)：x x 会朗读；会朗读； L(x)L(x)：x x 识字识字 D(x)D(

48、x)：x x 是海豚；是海豚； I(x)I(x)：x x 机灵机灵。 求证求证: :w 有些很机灵的东西有些很机灵的东西不会朗读。不会朗读。北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 55一阶谓词描述：一阶谓词描述：w( ( x)(R(x) )(R(x) L(x) L(x)； ( ( x)(D(x) )(D(x) L(x) L(x)w( ( x)(D(x) )(D(x) I(x) I(x)求证：求证： ( ( x)(I(x) )(I(x) R(x) R(x)推理策略推理策略实例（实例（2 2）子句集：子句集： S S0 0 = = R(x)

49、R(x) L(x), L(x), D(y)D(y) L(y), D(A), I(A), L(y), D(A), I(A), I(z)I(z) R(z)R(z) 求证：求证： S S0 0 |=|= 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 56推理策略推理策略实例实例- - 宽度优先策略宽度优先策略（1 1）s0s1 s2 s3 北京航空航天大学软件开发环境国家重点实验室北京航空航天大学软件开发环境国家重点实验室 Slide 57推理策略推理策略实例实例- - 宽度优先策略宽度优先策略（2 2）n归结策略运用过程：归结策略运用过程：w第一

50、级：原始子句集第一级：原始子句集 S0 中所有可能归结的子句对进行归结中所有可能归结的子句对进行归结，产生全部归结式，将其加到，产生全部归结式，将其加到 S0 中获新的归结子句集中获新的归结子句集 S1 = S0 1级归结式级归结式 。w 第第i i级：级：Si -1中所有可能归结的子句对进行归结，产生全部中所有可能归结的子句对进行归结，产生全部归结式，归结式，将其加到归结子句集将其加到归结子句集 Si -1中获新的归结子句集中获新的归结子句集 Si = Si -1 第第 i 级归结式级归结式 。n 归结策略特点：归结策略特点：w 策略完备，策略完备，搜索效率低。搜索效率低。北京航空航天大学软