人工智能ArtificialIntelligence学习培训课件.ppt

1、Artificial IntelligenceResolution:1 Graduate University,Chinese academy of Sciences.人工智能人工智能Artificial IntelligenceArtificial IntelligenceResolution:2 Graduate University,Chinese academy of Sciences.自动推理自动推理Artificial IntelligenceResolution:3 Graduate University,Chinese academy of Sciences.自动推理的理论和技

2、术是专家系统、程序推导、程自动推理的理论和技术是专家系统、程序推导、程序正确性证明、智能机器人等研究领域的重要基础序正确性证明、智能机器人等研究领域的重要基础。自动推理早期的工作主要集中在机器定理证明。自动推理早期的工作主要集中在机器定理证明。1930年年Herbrand为定理证明建立了一种重要方法，他的为定理证明建立了一种重要方法，他的方法奠定了机械定理证明的基础。方法奠定了机械定理证明的基础。机械定理证明的主要突破是机械定理证明的主要突破是1965年由年由J.A.Robinson做出做出的，他建立了所谓归结原理，使机械定理证明达到了应用的，他建立了所谓归结原理，使机械定理证明达到了应用阶段

3、。阶段。Artificial IntelligenceResolution:4 Graduate University,Chinese academy of Sciences.Agenda引言引言命题逻辑中的归结原理命题逻辑中的归结原理谓词逻辑中的归结原理谓词逻辑中的归结原理非单调推理非单调推理Artificial IntelligenceResolution:5 Graduate University,Chinese academy of Sciences.引言（引言（1）从一个或几个已知的判断从一个或几个已知的判断(前提前提)逻辑地推论出一个新的判逻辑地推论出一个新的判断断(结论结论)的思

4、维形式称为推理的思维形式称为推理,这是事物的客观联系在意识这是事物的客观联系在意识中的反映。中的反映。自动推理早期的工作主要集中在机器定理证明。机械定理自动推理早期的工作主要集中在机器定理证明。机械定理证明的中心问题是寻找判定公式是否是有效的（或是不一证明的中心问题是寻找判定公式是否是有效的（或是不一致的）通用程序。致的）通用程序。若按推理过程中推出的结论是否单调地增加，或者说推出若按推理过程中推出的结论是否单调地增加，或者说推出的结论是否越来越接近最终目标来划分，推理可以分为单的结论是否越来越接近最终目标来划分，推理可以分为单调推理和非单调推理。调推理和非单调推理。Artificial In

5、telligenceResolution:6 Graduate University,Chinese academy of Sciences.引言（引言（2）所谓单调推理是指在推理过程中随着推理的向前推进以及所谓单调推理是指在推理过程中随着推理的向前推进以及新知识的加入，推出的结论呈单调增加的趋势，并且越来新知识的加入，推出的结论呈单调增加的趋势，并且越来越接近最终目标，在推理过程中不会出现反复的情况，即越接近最终目标，在推理过程中不会出现反复的情况，即不会由于新知识的加入否定了前面推出的结论，从而使推不会由于新知识的加入否定了前面推出的结论，从而使推理又退回到前面的某一步。理又退回到前面的某

6、一步。所谓非单调推理是指在推理过程中由于新知识的加入，不所谓非单调推理是指在推理过程中由于新知识的加入，不仅没有加强已推出的结论，反而要否定它，使得推理退回仅没有加强已推出的结论，反而要否定它，使得推理退回到前面的某一步，重新开始。非单调推理是在知识不完全到前面的某一步，重新开始。非单调推理是在知识不完全的的情况下发生的。的的情况下发生的。Artificial IntelligenceResolution:7 Graduate University,Chinese academy of Sciences.引言（引言（3）在现实世界中存在大量不确定问题。不确定性来自人类的在现实世界中存在大量不确

7、定问题。不确定性来自人类的主观认识与客观实际之间存在差异。事物发生的随机性主观认识与客观实际之间存在差异。事物发生的随机性,人人类知识的不完全、不可靠、不精确和不一致类知识的不完全、不可靠、不精确和不一致,自然语言中自然语言中存在的模糊性和歧义性都反映了这种差异存在的模糊性和歧义性都反映了这种差异,都会带来不确都会带来不确定性。定性。针对不同的不确定性的起因针对不同的不确定性的起因,人们提出了不同的理论和推人们提出了不同的理论和推理方法。在下章中，我们将对不确定性推理进行讨论。理方法。在下章中，我们将对不确定性推理进行讨论。Artificial IntelligenceResolution:8

8、 Graduate University,Chinese academy of Sciences.引言（引言（4）证明的基本思想是：证明的基本思想是：设设F1、Fn、G为公式，为公式，G为为F1、Fn的逻辑推论，当的逻辑推论，当且仅当公式（且仅当公式（F1 Fn）G）是有效的是有效的 也可以采用反证法的思想：也可以采用反证法的思想：设设F1、Fn、G为公式，为公式，G为为F1、Fn的逻辑推论，当的逻辑推论，当且仅当公式（且仅当公式（F1 Fn G）是不可满足的是不可满足的 归结法的本质上就是一种反证法，它是在归结推理规则的归结法的本质上就是一种反证法，它是在归结推理规则的基础上实现的：基础上实

9、现的：为了证明一个命题为了证明一个命题P恒真，它证明其反命题恒真，它证明其反命题P恒假，即不恒假，即不存在使得存在使得 P为真的解释为真的解释 Artificial IntelligenceResolution:9 Graduate University,Chinese academy of Sciences.Agenda引言引言命题逻辑中的归结原理命题逻辑中的归结原理谓词逻辑中的归结原理谓词逻辑中的归结原理非单调推理非单调推理Artificial IntelligenceResolution:10 Graduate University,Chinese academy of Sciences

10、.命题逻辑中的归结原理命题逻辑中的归结原理子句和子句形子句和子句形归结归结 归结反演归结反演合理性和完备性合理性和完备性 归结反演的搜索策略归结反演的搜索策略Artificial IntelligenceResolution:11 Graduate University,Chinese academy of Sciences.子句和子句形子句和子句形（1）文字是原子或其否定文字是原子或其否定子句是文字的析取子句是文字的析取完备连接符集合：完备连接符集合：合取范式（合取范式（CNF）（L11 L1n1)(Lm1 Lmnm)析取范式（析取范式（DNF）（L11 L1n1)(Lm1 Lmnm)定理：

11、定理：对任意公式，都有与之等值的合取范式和析取范式对任意公式，都有与之等值的合取范式和析取范式转换方法：一般方法转换方法：一般方法 真值表方法真值表方法Artificial IntelligenceResolution:12 Graduate University,Chinese academy of Sciences.子句和子句形子句和子句形（2）一般方法一般方法 Eliminate implication signs by using the equivalent form using Reduce the scopes of signs by using DeMorgans law an

12、d by eliminating double signs Convert to CNF by using the associative and distributive laws.Artificial IntelligenceResolution:13 Graduate University,Chinese academy of Sciences.Resolution 对任意三个文字对任意三个文字 p、q 和和 r p r,q r p q 或者：或者：for C1=P C1,C2=P C2 P C1,P C2 C1 C2归结式：归结式：R(C1,C2)=C1 C2证明：证明：Artific

13、ial IntelligenceResolution:14 Graduate University,Chinese academy of Sciences.Resolution Refutations（1）定理证明的任务定理证明的任务:由前提由前提A1 A1 A2 A2 .AnAn推出结论推出结论B B即证明即证明:A1 A1 A2 A2 .AnAnB B 永真永真 转化为证明转化为证明:A1 A1 A2 A2 .An An B B为永假式为永假式 归结推理就是归结推理就是:从从A1 A1 A2 A2 .An An B B出发出发,使使用用归结推理规则归结推理规则来找出来找出矛盾矛盾,最后证明

14、定理最后证明定理A1 A1 A2 A2 .AnAnB B的成立的成立Artificial IntelligenceResolution:15 Graduate University,Chinese academy of Sciences.Resolution Refutations（2）归结方法是一种机械化的归结方法是一种机械化的,可在计算机上加以实现可在计算机上加以实现的推理方法的推理方法 可认为是一种反向推理形式可认为是一种反向推理形式 提供了一种自动定理证明的方法提供了一种自动定理证明的方法Artificial IntelligenceResolution:16 Graduate Uni

15、versity,Chinese academy of Sciences.Resolution Refutations（3）一般过程一般过程:1)建立子句集建立子句集S2)从子句集从子句集S出发出发,仅对仅对S的子句间使用归结推理规则的子句间使用归结推理规则3)如果得出空子句如果得出空子句 ,则结束则结束;否则转下一步否则转下一步4)将所得归结式仍放入将所得归结式仍放入S中中5)对新的子句集使用归结推理规则对新的子句集使用归结推理规则6)转转(3)空子句不含有文字空子句不含有文字,它不能被任何解释满足它不能被任何解释满足,所以空子句是永所以空子句是永假的假的,不可满足的不可满足的归结过程出现空子

16、句归结过程出现空子句,说明出现互补子句对说明出现互补子句对,说明说明S中有矛盾中有矛盾,因此因此S是不可满足的是不可满足的.Artificial IntelligenceResolution:17 Graduate University,Chinese academy of Sciences.Resolution Refutations（4）例子例子:证明证明(P Q)Q p 首先建立子句集首先建立子句集:(P Q)Q (P)(P Q)Q P S=P Q,Q,P 对对S作归结作归结:(1)P Q(2)Q(3)P(4)P (1)(2)归结归结(5)(3)(4)归结归结Artificial Int

17、elligenceResolution:18 Graduate University,Chinese academy of Sciences.Soundness and Completeness 归结原理是合理的归结原理是合理的 归结原理是完备的归结原理是完备的Artificial IntelligenceResolution:19 Graduate University,Chinese academy of Sciences.Resolution Refutation Search Strategies 有序策略（有序策略（Order strategiesOrder strategies）R

18、efinement strategies Refinement strategies1.1.支持集（支持集（Set of supportSet of support）:每次归结时，参与归结的子句中至少应有一个是由目标公式的每次归结时，参与归结的子句中至少应有一个是由目标公式的否定所得到的子句，或者是它们的后裔否定所得到的子句，或者是它们的后裔该策略是完备的该策略是完备的2.2.线性输入（线性输入（Linear InputLinear Input）：参与归结的两个子句中至少有一个是初始子句集中的子句参与归结的两个子句中至少有一个是初始子句集中的子句该策略是不完备的该策略是不完备的3.3.祖先过滤

19、（祖先过滤（Ancestry FilteringAncestry Filtering）：参与归结的两个子句中至少有一个是初始子句集中的句子，或参与归结的两个子句中至少有一个是初始子句集中的句子，或者是另一个子句的祖先者是另一个子句的祖先该策略是完备的该策略是完备的Artificial IntelligenceResolution:20 Graduate University,Chinese academy of Sciences.Agenda引言引言命题逻辑中的归结原理命题逻辑中的归结原理谓词逻辑中的归结原理谓词逻辑中的归结原理非单调推理非单调推理Artificial Intelligence

20、Resolution:21 Graduate University,Chinese academy of Sciences.谓词逻辑归结方法谓词逻辑归结方法 子句形子句形 归结原理归结原理 归结的完备性归结的完备性Artificial IntelligenceResolution:22 Graduate University,Chinese academy of Sciences.子句形子句形-SKOLEM标准型标准型 前束范式前束范式 (Q1x1)(Qnxn)M(x1,xn)前束形前束形=(前前 缀缀 )母母 式式 量词串量词串 无量词公式无量词公式定理：任何公式定理：任何公式G都等价于一个

21、前束范式都等价于一个前束范式Skolem函数：函数：存在量词不出现在全称量词的辖域内存在量词不出现在全称量词的辖域内,此时只要用一个新的个体常量此时只要用一个新的个体常量(称为称为Skolem常量常量)替换受该存在量词约束的变元就可消去存在量词替换受该存在量词约束的变元就可消去存在量词 存在量词位于一个或多个全称量词的辖域内存在量词位于一个或多个全称量词的辖域内.此时需要此时需要Skolem函数函数,该函数的变元就是由那些全称量词所约束的全称量词量化的变量该函数的变元就是由那些全称量词所约束的全称量词量化的变量.Skolem函数所使用的函数符号必须是新的函数所使用的函数符号必须是新的.Arti

22、ficial IntelligenceResolution:23 Graduate University,Chinese academy of Sciences.子句形子句形-SKOLEM标准型标准型 Skolem标准型：标准型：没有存在量词的公式。没有存在量词的公式。设设G是一阶逻辑中的公式，将其化为是一阶逻辑中的公式，将其化为Skolem标标准型，母式准型，母式M给出的子句集给出的子句集S称为公式称为公式G的子句的子句集集Artificial IntelligenceResolution:24 Graduate University,Chinese academy of Sciences.

23、子句形子句形化子句集化子句集-1 谓词公式化为子句形的步骤谓词公式化为子句形的步骤 x P(x)y P(y)P(f(x,y)y Q(x,y)P(y)(1)消去蕴含符号消去蕴含符号:PQ P Q x P(x)yP(y)P(f(x,y)y Q(x,y)P(y)(2)减少否定符号的辖域减少否定符号的辖域,把把“”移到紧靠谓词的位置上移到紧靠谓词的位置上 (P)P (P Q)P Q (P Q)P Q (x)P (x)P (x)P (x)P x P(x)y P(y)P(f(x,y)y Q(x,y)P(y)Artificial IntelligenceResolution:25 Graduate Univ

24、ersity,Chinese academy of Sciences.子句形子句形化子句集化子句集-2(3)变量标准化变量标准化:重新命名变元名重新命名变元名,使不同量词约束的变元有不使不同量词约束的变元有不同的名字同的名字.xP(x)y P(y)P(f(x,y)w Q(x,w)P(w)(4)消去存在量词消去存在量词:xP(x)yP(y)P(f(x,y)Q(x,g(x)P(g(x)Artificial IntelligenceResolution:26 Graduate University,Chinese academy of Sciences.子句形子句形化子句集化子句集-3(5)化为前束

25、形化为前束形:把所有的全称量词移到公式的左边把所有的全称量词移到公式的左边,并使每个量词的辖域并使每个量词的辖域包含这个量词后面公式的整个部分包含这个量词后面公式的整个部分.即得前束形即得前束形 上例变为上例变为:x y P(x)P(y)P(f(x,y)Q(x,g(x)P(g(x)(6)把母式化为合取范式把母式化为合取范式:上例变为上例变为:x y P(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(x)P(g(x)Artificial IntelligenceResolution:27 Graduate University,Chinese academy of Sciences.子

26、句形子句形化子句集化子句集-4(7)消去全称量词消去全称量词:P(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(x)P(g(x)(8)消去连结词符号消去连结词符号 P(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(x)P(g(x)(9)更换变量名称更换变量名称:对变元更名对变元更名,使不同子句中的变元不同名使不同子句中的变元不同名.P(x1)P(y)P(f(x1,y)P(x2)Q(x2,g(x2)P(x3)P(g(x3)Artificial IntelligenceResolution:28 Graduate University,Chinese academy of Sc

27、iences.子句形子句形化子句集化子句集-6 一个子句内的文字可含有变量一个子句内的文字可含有变量,但这些变量总是被理解为全称但这些变量总是被理解为全称量词量化的变量量词量化的变量 G与其子句集与其子句集S并不等值并不等值.但是在不可满足的意义下两者是等但是在不可满足的意义下两者是等价的价的.而且而且G是是S的逻辑推论的逻辑推论,SG.反过来不成立反过来不成立Artificial IntelligenceResolution:29 Graduate University,Chinese academy of Sciences.谓词逻辑的子句形谓词逻辑的子句形-定理定理 定理定理:若若G是给定

28、的公式是给定的公式,而相应的子句集为而相应的子句集为S,则则G是不可满足是不可满足的当且仅当的当且仅当S是不可满足的是不可满足的 推论：设推论：设G=G1 Gn,Si 是是 Gi的的Skolem标准型，令标准型，令S=Si Sn，则，则，G是不可满足的当且仅当是不可满足的当且仅当S是不可满足的是不可满足的。Artificial IntelligenceResolution:30 Graduate University,Chinese academy of Sciences.示例示例-1 例例1:证明梯形的对角线与上下底构成的内错角相等证明梯形的对角线与上下底构成的内错角相等 设给定梯形的顶点依

29、次为设给定梯形的顶点依次为:a,b,c,d.T(x,y,u,v):表示以表示以xy为上底为上底,uv为下底的梯形为下底的梯形P(x,y,u,v):表示表示xy平行于平行于uvE(x,y,z,u,v,w):表示表示 xyz=uvw问题的逻辑描述和相应的子句集为问题的逻辑描述和相应的子句集为:A1:(x)(y)(u)(v)(T(x,y,u,v)P(x,y,u,v)SA1:T(x,y,u,v)P(x,y,u,v)A2:(x)(y)(u)(v)(P(x,y,u,v)E(x,y,v,u,v,y)SA2:P(x,y,u,v)E(x,y,v,u,v,y)Artificial IntelligenceReso

30、lution:31 Graduate University,Chinese academy of Sciences.示例示例-1(续）续）A3:T(a,b,c,d)(已知已知)SA3:T(a,b,c,d)B:E(a,b,d,c,d,b)(要证的结论要证的结论)SB:E(a,b,d,c,d,b)因此因此:S=SA1 SA2 SA3 SBArtificial IntelligenceResolution:32 Graduate University,Chinese academy of Sciences.示例示例-2 例例2:对所有的对所有的x,y,z来说来说,如果如果y是是x父亲父亲,z是是y的

31、父亲的父亲,则则z是是x的的祖父祖父.又知道每个人都有父亲又知道每个人都有父亲,试问对某个人来说试问对某个人来说,谁是他的祖谁是他的祖父父?引入谓词引入谓词:P(x,y):表示表示x是是y的父亲的父亲Q(x,y):表示表示x是是y的祖父的祖父A1:(x)(y)(z)(P(x,y)P(y,z)Q(x,z)SA1:P(x,y)P(y,z)Q(x,z)A2:(y)(x)P(x,y)SA2:P(f(y),y)Artificial IntelligenceResolution:33 Graduate University,Chinese academy of Sciences.示例示例-2（续）（续）B

32、:(x)(y)Q(x,y)(要证的结论要证的结论)SB:Q(x,y)ANS(x)其中其中ANS(x)是人为增加的是人为增加的,在推理过程中在推理过程中,ANS(x)变量变量x同同Q(x,y)中的中的x作同样的变换作同样的变换,当推理结束的时候当推理结束的时候,ANS(x)中中的变量的变量x便给出了问题的解答便给出了问题的解答因此因此:S=SA1 SA2 SBArtificial IntelligenceResolution:34 Graduate University,Chinese academy of Sciences.谓词逻辑中的归结原理谓词逻辑中的归结原理置换与合一置换与合一归结式归结

33、式归结反演归结反演Artificial IntelligenceResolution:35 Graduate University,Chinese academy of Sciences.置换(Substitution)（1）例：例：C1：P(x)Q(x)C2：P(f(x)R(x)没有互补对没有互补对;例：例：C1：P(y)Q(y)y/x C1：P(f(x)Q(f(x)f(x)/y C3：R(x)Q(f(x)Artificial IntelligenceResolution:36 Graduate University,Chinese academy of Sciences.置换(2）置换和合

34、一是为了处理谓词逻辑中子句之间的模式匹配而引进.定义:置换是形如 t1/v1,t2/v2,tn/vn 的一个有限集.其中vi是变量,而ti是不同于vi的项(常量,变量,函数),且vi vj(i j),i,j=1,n 例子：例子：a/x,w/y,f(s)/z,g(x)/x是置换是置换;x/x,y/f(x)不是置换不是置换;Artificial IntelligenceResolution:37 Graduate University,Chinese academy of Sciences.置换-（3）定义：不含任何元素的置换称为空置换，记为 定义:设=t1/v1,t2/v2,tn/vn是一个置换

35、，E是一个表达式。将E中出现的每一个变量符号vi（1 i n）,都用项ti置换，这样得到的表达式记为E，称E 为E的例。Artificial IntelligenceResolution:38 Graduate University,Chinese academy of Sciences.置换-（4）例子：例子：E=P(x,y,z),=a/x,f(b)/y,c/z E=P(a,f(b),c)E=P(x,g(y),h(x,z),=a/x,f(b)/y,g(w)/z E=P(a,g(f(b),h(a,g(w)E=P(x,y,z),=y/x,z/y E=P(y,z,z).EP(z,z,z).(同时同

36、时)Artificial IntelligenceResolution:39 Graduate University,Chinese academy of Sciences.置换的复合（乘积）（1）例子例子:E=P(x,y,z)=a/x,f(z)/y,w/z E=P(a,f(z),w)=t/z,g(b)/w E=P(a,f(t),g(b)=a/x,f(t)/y,g(b)/zArtificial IntelligenceResolution:40 Graduate University,Chinese academy of Sciences.置换的复合（乘积）（2）定义：设=t1/x1,t2/x

37、2,tn/xn和 =u1/y1,u2/y2,um/ym是两个置换,也是一个置换,可定义为:先作置换:t1 /x1,t2 /x2,tn /xn,u1/y1,u2/y2,um/ym若:yi (x1,x2,xn)则删除ui/yi若:ti =xi,则删除ti =xi所得的置换称为 和的复合或乘积,记为 Artificial IntelligenceResolution:41 Graduate University,Chinese academy of Sciences.置换的复合（乘积）-（3）定理：1.设和是两个置换,E是表达式，则 E()=(E)2.设,是三个置换,则有:置换满足结合率:()=()

38、置换的交换率不成立3.=Artificial IntelligenceResolution:42 Graduate University,Chinese academy of Sciences.置换的复合（乘积）-（4）=a/x,=b/x=a/x=b/x Artificial IntelligenceResolution:43 Graduate University,Chinese academy of Sciences.合一（Unification）（1）定义:设有公式集E=E1,.,En和置换,使得:E1=E2=En 则称E1,.,En是可合一的,并且称为一合一置换.也称为 E1,En的合

39、一子(unifier).定义：如果对E1,En存在这样的合一子,则称集合E1,En是可合一的.Artificial IntelligenceResolution:44 Graduate University,Chinese academy of Sciences.合一（Unification）（2）例1:E=P(a,y),P(x,f(b),=a/x,f(b)/y.E=P(a,b),P(x,f(b)合一子不一定唯一 E=P(a,y),P(x,f(b)1=a/x,f(b)/y (唯一唯一)E=P(x,y),P(x,f(b)1=a/x,f(b)/y (不唯一不唯一)2=b/x,f(b)/yArtif

40、icial IntelligenceResolution:45 Graduate University,Chinese academy of Sciences.最一般合一（1）定义:设是公式集E的一个合一,如果对于任一个合一,都存在置换使得:=,则称是公式集E的最一般合一置换,记为mgu(most general unifier)Artificial IntelligenceResolution:46 Graduate University,Chinese academy of Sciences.最一般合一（2）例子:E=P(x,y),P(x,f(b)1=a/x,f(b)/y 2=b/x,f(

41、b)/y =f(b)/y 1=a/x 2=b/xArtificial IntelligenceResolution:47 Graduate University,Chinese academy of Sciences.差异集合 设W是非空表达式集合，W的差异集合D定义如下：首先找出W的所有表达式中不是都相同的第一个符号，然后从W的每个表达式中抽出占有这个符号位置的子表达式，所有这些子表达式组成的集合就是W的差异集合D。1.若D中无变量符号，则W是不可合一的2.若D中只有一个元素，则W是不可合一的3.若D中的变量符号x和t，且x出现在t中，则W是不可合一的例子:W=P(x,f(y,z),z，w)

42、,P(x,a),P(x,g(z),z,b)D=f(y,z),a,g(z)Artificial IntelligenceResolution:48 Graduate University,Chinese academy of Sciences.合一算法（1）(1)令k=0,W0=W(W=E1,E2),0=(2)如果Wk已经合一,则算法停止,k=mgu 否则，求出Wk的差异集Dk(3)如果如果Dk中存在元素中存在元素xk,tk,且且xk不在不在tk中出现中出现,则转(4)；否则不可合一，停止(4)令 k+1=k tk/xk W k+1=W ktk/xk=W k+1(5)k=k+1 然后转(2)Ar

43、tificial IntelligenceResolution:49 Graduate University,Chinese academy of Sciences.合一算法（2）换名:P(f(x),x),P(x,a);如果不换名：如果不换名：D=f(x),x.换名换名:P(f(y),y),P(x,a);mgu:f(a)/x,a/yArtificial IntelligenceResolution:50 Graduate University,Chinese academy of Sciences.合一算法（3）求W=P(a,x,f(g(y),P(z,f(z),f(u)的mgu.D0=a,z.

44、1=a/z=a/z.W1=W0 1=P(a,x,f(g(y),P(a,f(a),f(u)D1=x,f(a).2=1 f(a)/x=a/z,f(a)/x.W2=W1 2=P(a,f(a),f(g(y),P(a,f(a),f(u)D2=g(y),u.3=2 g(y)/u=a/z,f(a)/x,g(y)/u W3=W2 3=P(a,f(a),f(g(y)3是是mgu.Artificial IntelligenceResolution:51 Graduate University,Chinese academy of Sciences.合一算法（4）求W=Q(f(a),g(x),Q(y,y)的mgu.

45、D0=f(a),y.1=f(a)/y=f(a)/y.W1=W0 1=Q(f(a),g(x),Q(f(a),f(a)D1=g(x),f(a).不可合一不可合一,没有没有mgu.Artificial IntelligenceResolution:52 Graduate University,Chinese academy of Sciences.合一算法（5）求W=P(f(y),y),P(x,a)的mgu.D0=f(y),x.1=f(y)/x=f(y)/x.W1=W0 1=P(f(y),y),P(f(y),a)D1=y,a.2=1a/y=f(y)/x a/y=f(a)/x,a/y.W2=W1 2=

46、P(f(a),a)2是mgu.Artificial IntelligenceResolution:53 Graduate University,Chinese academy of Sciences.合一算法（6）性质：1.若W是关于表达式的有限非空可合一集合，则合一算法将在第（2）步结束，并且最后的 k是W的mgu。2.若一组表达式E1,En 是可合一的，则它们的mgu除了相差一个改名外，是唯一确定。Artificial IntelligenceResolution:54 Graduate University,Chinese academy of Sciences.归结式归结式定义:设C1

47、和C2是两个无公共变量的子句,L1和L2 分别是C1 和C2 的文字,如果L1和L2 有mgu:,则:(C1-L1)(C2-L2)称为C1和 C2 的一个二元归结式,而L1 L2称为被归结的文字 若R(C1,C2)是C1,C2的二元归结式,则:C1 C2=R(C1,C2)Artificial IntelligenceResolution:55 Graduate University,Chinese academy of Sciences.归结式-例子（1）C1:P(x)Q(x)C2:P(a)R(x)重命名重命名C2:P(a)R(y)L1=P(x),L2=P(a)L1与与L2有有mgu =a/x

48、(C1 L1)(C2 L2)=(P(a),Q(a)P(a)(P(a),R(y)P(a)=Q(a)R(y)=Q(a),R(y)Q(a)R(y)是是C1与与C2的的二元归结式二元归结式.Artificial IntelligenceResolution:56 Graduate University,Chinese academy of Sciences.归结式-例子（2）C1=P(x)Q(x)C2=P(g(y)Q(b)R(x)1=g(y)/x:R(C1,C2)=Q(g(y)Q(b)R(x)2=b/x:R(C1,C2)=P(g(y)P(b)R(x)Artificial IntelligenceRes

49、olution:57 Graduate University,Chinese academy of Sciences.归结式因子定义：定义：如果一个子句C的几个文字有mgu,则C 称为子句C的因子例子 设C=P(x)P(f(y)Q(x)假设=f(y)/x,则:C=P(f(y)Q(f(y)Artificial IntelligenceResolution:58 Graduate University,Chinese academy of Sciences.归结式定义:设C1和C2是无公共变量的子句,其归结式是下列二元归结式之一:(1)C1和C2的二元归结式(2)C1的因子和C2的二元归结式(3)

50、C1和C2的因子的二元归结式(4)C1的因子和C2的因子的二元归结式该归结式仍记为R(C1,C2)Artificial IntelligenceResolution:59 Graduate University,Chinese academy of Sciences.归结式-2例:C1=P(x)P(f(y)Q(g(y)C2=P(f(g(x)Q(b)C1的因子为:=f(y)/x,C1=P(f(y)Q(g(y)则:R(C1,C2)=Q(g(g(x)Q(b)Artificial IntelligenceResolution:60 Graduate University,Chinese academy