《第四章自动推理(ppt)》由会员分享，可在线阅读，更多相关《第四章自动推理(ppt)（126页珍藏版）》请在金锄头文库上搜索。
1、ArtificialIntelligenceResolution:1 Graduate University , Chinese academy of Sciences. 自动推理自动推理ArtificialIntelligenceResolution:2 Graduate University , Chinese academy of Sciences. 自动推理的理论和技术是专家系统、程序推导、程自动推理的理论和技术是专家系统、程序推导、程序正确性证明、智能机器人等研究领域的重要基础。序正确性证明、智能机器人等研究领域的重要基础。自动推理早期的工作主要集中在机器定理证明。自动推理早期的工作
2、主要集中在机器定理证明。1930年年Herbrand为定理证明建立了一种重要方法，他的为定理证明建立了一种重要方法，他的方法奠定了机械定理证明的基础。方法奠定了机械定理证明的基础。机械定理证明的主要突破是机械定理证明的主要突破是1965年由年由J.A.Robinson做出做出的，他建立了所谓归结原理，使机械定理证明达到了应用的，他建立了所谓归结原理，使机械定理证明达到了应用阶段。阶段。ArtificialIntelligenceResolution:3 Graduate University , Chinese academy of Sciences. Agenda引言引言命题逻辑中的归结原理
3、命题逻辑中的归结原理谓词逻辑中的归结原理谓词逻辑中的归结原理非单调推理非单调推理ArtificialIntelligenceResolution:4 Graduate University , Chinese academy of Sciences. 引言（引言（1）从一个或几个已知的判断从一个或几个已知的判断(前提前提)逻辑地推论出一个新的判逻辑地推论出一个新的判断断(结论结论)的思维形式称为推理的思维形式称为推理,这是事物的客观联系在意识这是事物的客观联系在意识中的反映。中的反映。自动推理早期的工作主要集中在机器定理证明。机械定理自动推理早期的工作主要集中在机器定理证明。机械定理证明的中心
4、问题是寻找判定公式是否是有效的（或是不一证明的中心问题是寻找判定公式是否是有效的（或是不一致的）通用程序。致的）通用程序。若按推理过程中推出的结论是否单调地增加，或者说推出若按推理过程中推出的结论是否单调地增加，或者说推出的结论是否越来越接近最终目标来划分，推理可以分为单的结论是否越来越接近最终目标来划分，推理可以分为单调推理和非单调推理。调推理和非单调推理。ArtificialIntelligenceResolution:5 Graduate University , Chinese academy of Sciences. 引言（引言（2）所谓单调推理是指在推理过程中随着推理的向前推进以及
5、所谓单调推理是指在推理过程中随着推理的向前推进以及新知识的加入，推出的结论呈单调增加的趋势，并且越来新知识的加入，推出的结论呈单调增加的趋势，并且越来越接近最终目标，在推理过程中不会出现反复的情况，即越接近最终目标，在推理过程中不会出现反复的情况，即不会由于新知识的加入否定了前面推出的结论，从而使推不会由于新知识的加入否定了前面推出的结论，从而使推理又退回到前面的某一步。理又退回到前面的某一步。所谓非单调推理是指在推理过程中由于新知识的加入，不所谓非单调推理是指在推理过程中由于新知识的加入，不仅没有加强已推出的结论，反而要否定它，使得推理退回仅没有加强已推出的结论，反而要否定它，使得推理退回到
6、前面的某一步，重新开始。非单调推理是在知识不完全到前面的某一步，重新开始。非单调推理是在知识不完全的的情况下发生的。的的情况下发生的。ArtificialIntelligenceResolution:6 Graduate University , Chinese academy of Sciences. 引言（引言（3）在现实世界中存在大量不确定问题。不确定性来自人类的在现实世界中存在大量不确定问题。不确定性来自人类的主观认识与客观实际之间存在差异。事物发生的随机性主观认识与客观实际之间存在差异。事物发生的随机性,人人类知识的不完全、不可靠、不精确和不一致类知识的不完全、不可靠、不精确和不一致
7、,自然语言中存自然语言中存在的模糊性和歧义性都反映了这种差异在的模糊性和歧义性都反映了这种差异,都会带来不确定都会带来不确定性。性。针对不同的不确定性的起因针对不同的不确定性的起因,人们提出了不同的理论和推人们提出了不同的理论和推理方法。在下章中，我们将对不确定性推理进行讨论。理方法。在下章中，我们将对不确定性推理进行讨论。ArtificialIntelligenceResolution:7 Graduate University , Chinese academy of Sciences. 引言（引言（4）证明的基本思想是：证明的基本思想是： 设设F1、Fn、G为公式，为公式，G为为F1、F
8、n的逻辑推论，当的逻辑推论，当且仅当公式（且仅当公式（F1 Fn）G）是有效的是有效的也可以采用反证法的思想：也可以采用反证法的思想： 设设F1、Fn、G为公式，为公式，G为为F1、Fn的逻辑推论，当的逻辑推论，当且仅当公式（且仅当公式（F1 Fn G）是不可满足的是不可满足的归结法的本质上就是一种反证法，它是在归结推理规则的归结法的本质上就是一种反证法，它是在归结推理规则的基础上实现的：基础上实现的： 为了证明一个命题为了证明一个命题P恒真，它证明其反命题恒真，它证明其反命题P恒假，即不恒假，即不存在使得存在使得 P为真的解释为真的解释ArtificialIntelligenceResolu
9、tion:8 Graduate University , Chinese academy of Sciences. Agenda引言引言命题逻辑中的归结原理命题逻辑中的归结原理谓词逻辑中的归结原理谓词逻辑中的归结原理非单调推理非单调推理ArtificialIntelligenceResolution:9 Graduate University , Chinese academy of Sciences. 命题逻辑中的归结原理命题逻辑中的归结原理子句和子句形子句和子句形归结归结归结反演归结反演合理性和完备性合理性和完备性归结反演的搜索策略归结反演的搜索策略ArtificialIntelligen
10、ceResolution:10 Graduate University , Chinese academy of Sciences. 子句和子句形子句和子句形（1）文字是原子或其否定文字是原子或其否定子句是文字的析取子句是文字的析取完备连接符集合：完备连接符集合：合取范式（合取范式（CNF）（L11 L1n1) (Lm1 Lmnm)析取范式（析取范式（DNF）（L11 L1n1) (Lm1 Lmnm)定理：定理： 对任意公式，都有与之等值的合取范式和析取范式对任意公式，都有与之等值的合取范式和析取范式转换方法：一般方法转换方法：一般方法真值表方法真值表方法ArtificialIntellige
11、nceResolution:11 Graduate University , Chinese academy of Sciences. 子句和子句形子句和子句形（2）一般方法一般方法Eliminateimplicationsignsbyusingtheequivalentformusing ReducethescopesofsignsbyusingDeMorganslawandbyeliminatingdoublesignsConverttoCNFbyusingtheassociativeanddistributivelaws.ArtificialIntelligenceResolution:
12、12 Graduate University , Chinese academy of Sciences. Resolution 对任意三个文字对任意三个文字p、q和和rp r,q rp q或者：或者：forC1=P C1,C2=P C2P C1,P C2C1 C2归结式：归结式：R(C1,C2)=C1 C2证明：证明：ArtificialIntelligenceResolution:13 Graduate University , Chinese academy of Sciences. ResolutionRefutations（1）定理证明的任务定理证明的任务: :由前提由前提A1 A1
13、 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出发出发, ,使使用用归结推理规则归结推理规则来找出来找出矛盾矛盾, ,最后证明定理最后证明定理A1 A1 A2 A2 . . AnAnB B的成立的成立ArtificialIntelligenceResolution:14 Graduate University , Chinese academ
14、y of Sciences. ResolutionRefutations（2）归结方法是一种机械化的归结方法是一种机械化的,可在计算机上加以实现可在计算机上加以实现的推理方法的推理方法可认为是一种反向推理形式可认为是一种反向推理形式提供了一种自动定理证明的方法提供了一种自动定理证明的方法ArtificialIntelligenceResolution:15 Graduate University , Chinese academy of Sciences. ResolutionRefutations（3）一般过程一般过程:1)建立子句集建立子句集S2)从子句集从子句集S出发出发,仅对仅对S的子
15、句间使用归结推理规则的子句间使用归结推理规则3)如果得出空子句如果得出空子句 ,则结束则结束;否则转下一步否则转下一步4)将所得归结式仍放入将所得归结式仍放入S中中5)对新的子句集使用归结推理规则对新的子句集使用归结推理规则6)转转(3)空子句不含有文字空子句不含有文字,它不能被任何解释满足它不能被任何解释满足,所以空子句是所以空子句是永假的永假的,不可满足的不可满足的归结过程出现空子句归结过程出现空子句,说明出现互补子句对说明出现互补子句对,说明说明S中有矛盾中有矛盾,因此因此S是不可满足的是不可满足的.ArtificialIntelligenceResolution:16 Graduate
16、 University , Chinese academy of Sciences. ResolutionRefutations（4）例子例子:证明证明(PQ) Qp首先建立子句集首先建立子句集:(PQ) Q (P)(P Q) Q PS=P Q,Q,P对对S作归结作归结:(1)P Q(2)Q(3)P(4)P(1)(2)归结归结(5) (3)(4)归结归结ArtificialIntelligenceResolution:17 Graduate University , Chinese academy of Sciences. SoundnessandCompleteness归结原理是合理的归结原
17、理是合理的归结原理是完备的归结原理是完备的ArtificialIntelligenceResolution:18 Graduate University , Chinese academy of Sciences. ResolutionRefutationSearchStrategies有序策略（有序策略（Order strategiesOrder strategies） Refinement strategies Refinement strategies1.1.支持集（支持集（Set of supportSet of support）: : 每次归结时，参与归结的子句中至少应有一个是由目标
18、公式的每次归结时，参与归结的子句中至少应有一个是由目标公式的否定所得到的子句，或者是它们的后裔否定所得到的子句，或者是它们的后裔该策略是完备的该策略是完备的2.2.线性输入（线性输入（Linear InputLinear Input）：参与归结的两个子句中至少有一个是初始子句集中的子句参与归结的两个子句中至少有一个是初始子句集中的子句该策略是不完备的该策略是不完备的3.3.祖先过滤（祖先过滤（Ancestry FilteringAncestry Filtering） ：参与归结的两个子句中至少有一个是初始子句集中的句子，或参与归结的两个子句中至少有一个是初始子句集中的句子，或者是另一个子句的祖
19、先者是另一个子句的祖先该策略是完备的该策略是完备的ArtificialIntelligenceResolution:19 Graduate University , Chinese academy of Sciences. Agenda引言引言命题逻辑中的归结原理命题逻辑中的归结原理谓词逻辑中的归结原理谓词逻辑中的归结原理非单调推理非单调推理ArtificialIntelligenceResolution:20 Graduate University , Chinese academy of Sciences. 谓词逻辑归结方法谓词逻辑归结方法子句形子句形归结原理归结原理归结的完备性归结的完备
20、性ArtificialIntelligenceResolution:21 Graduate University , Chinese academy of Sciences. 子句形子句形-SKOLEM标准型标准型 前束范式前束范式(Q1x1)(Qnxn)M(x1,xn)前束形前束形=(前前缀缀)母母式式量词串量词串无量词公式无量词公式定理：任何公式定理：任何公式G都等价于一个前束范式都等价于一个前束范式Skolem函数：函数：存在量词不出现在全称量词的辖域内存在量词不出现在全称量词的辖域内,此时只要用一个新的个体常量此时只要用一个新的个体常量(称为称为Skolem常量常量)替换受该存在量词约
21、束的变元就可消去存在量词替换受该存在量词约束的变元就可消去存在量词存在量词位于一个或多个全称量词的辖域内存在量词位于一个或多个全称量词的辖域内.此时需要此时需要Skolem函数函数,该函数的变元就是由那些全称量词所约束的全称量词量化的变量该函数的变元就是由那些全称量词所约束的全称量词量化的变量.Skolem函数所使用的函数符号必须是新的函数所使用的函数符号必须是新的.ArtificialIntelligenceResolution:22 Graduate University , Chinese academy of Sciences. 子句形子句形-SKOLEM标准型标准型Skolem标准型
22、：标准型：没有存在量词的公式。没有存在量词的公式。设设G是一阶逻辑中的公式，将其化为是一阶逻辑中的公式，将其化为Skolem标标准型，母式准型，母式M给出的子句集给出的子句集S称为公式称为公式G的子句的子句集集ArtificialIntelligenceResolution:23 Graduate University , Chinese academy of Sciences. 子句形子句形化子句集化子句集-1谓词公式化为子句形的步骤谓词公式化为子句形的步骤 x P(x) yP(y)P(f(x,y) yQ(x,y)P(y)(1)消去蕴含符号消去蕴含符号:PQP Q xP(x) yP(y) P
23、(f(x,y) yQ(x,y) P(y)(2)减少否定符号的辖域减少否定符号的辖域,把把“”移到紧靠谓词的位置上移到紧靠谓词的位置上(P)P(P Q)P Q(P Q)P Q( x)P( x)P( x)P( x)P xP(x) yP(y) P(f(x,y) yQ(x,y) P(y)ArtificialIntelligenceResolution:24 Graduate University , Chinese academy of Sciences. 子句形子句形化子句集化子句集-2(3)变量标准化变量标准化:重新命名变元名重新命名变元名,使不同量词约束的变元有不使不同量词约束的变元有不同的名字
24、同的名字. xP(x) yP(y) P(f(x,y)wQ(x,w) P(w)(4)消去存在量词消去存在量词: xP(x) yP(y) P(f(x,y) Q(x,g(x) P(g(x)ArtificialIntelligenceResolution:25 Graduate University , Chinese academy of Sciences. 子句形子句形化子句集化子句集-3(5)化为前束形化为前束形:把所有的全称量词移到公式的左边把所有的全称量词移到公式的左边,并使每个量词的辖域并使每个量词的辖域包含这个量词后面公式的整个部分包含这个量词后面公式的整个部分.即得前束形即得前束形上例
25、变为上例变为: x yP(x) P(y) P(f(x,y) Q(x,g(x) P(g(x)(6)把母式化为合取范式把母式化为合取范式:上例变为上例变为: x yP(x) P(y) P(f(x,y) P(x) Q(x,g(x) P(x) P(g(x)ArtificialIntelligenceResolution:26 Graduate University , Chinese academy of Sciences. 子句形子句形化子句集化子句集-4(7)消去全称量词消去全称量词:P(x) P(y) P(f(x,y) P(x) Q(x,g(x) P(x) P(g(x)(8)消去连结词符号消去连
26、结词符号 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)ArtificialIntelligenceResolution:27 Graduate University , Chinese academy of Sciences. 子句形子句形化子句集化子句集-6一个子句内的文字可含有变量一个子句内的文字可含有变量,但这些变量总是被理解为全但这些变量总是被理解
27、为全称量词量化的变量称量词量化的变量G与其子句集与其子句集S并不等值并不等值.但是在不可满足的意义下两者是等但是在不可满足的意义下两者是等价的价的.而且而且G是是S的逻辑推论的逻辑推论,SG.反过来不成立反过来不成立ArtificialIntelligenceResolution:28 Graduate University , Chinese academy of Sciences. 谓词逻辑的子句形谓词逻辑的子句形-定理定理定理定理:若若G是给定的公式是给定的公式,而相应的子句集为而相应的子句集为S,则则G是不可满是不可满足的当且仅当足的当且仅当S是不可满足的是不可满足的推论：设推论：设G
28、=G1 Gn,Si是是Gi的的Skolem标准型，令标准型，令S=Si Sn，则，则，G是不可满足的当且仅当是不可满足的当且仅当S是不可满足的。是不可满足的。ArtificialIntelligenceResolution:29 Graduate University , Chinese academy of Sciences. 示例示例-1例例1:证明梯形的对角线与上下底构成的内错角相等证明梯形的对角线与上下底构成的内错角相等设给定梯形的顶点依次为设给定梯形的顶点依次为:a,b,c,d.T(x,y,u,v):表示以表示以xy为上底为上底,uv为下底的梯形为下底的梯形P(x,y,u,v):表示
29、表示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)ArtificialIntelligenceResolution:30 Graduate University , Chinese academy of Sciences. 示例示例
30、-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 SBArtificialIntelligenceResolution:31 Graduate University , Chinese academy of Sciences. 示例示例-2例例2:对所有的对所有的x,y,z来说来说,如果如果y是是x父亲父亲,z是是y的父亲的父亲,则则z是是x的祖父的祖父.又知道每个人都有父亲又知道每个人都有父亲,试问对某个人来说试问对某个人来说,谁是他谁
31、是他的祖父的祖父?引入谓词引入谓词: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)ArtificialIntelligenceResolution:32 Graduate University , Chinese academy of Sciences. 示例示例-2（续）（续）B:( x)( y)Q(x,y)(要证的结论要证的结论)SB:Q(x,y) ANS(x)其中其中ANS(
32、x)是人为增加的是人为增加的,在推理过程中在推理过程中,ANS(x)变量变量x同同Q(x,y)中的中的x作同样的变换作同样的变换,当推理结束的时候当推理结束的时候,ANS(x)中中的变量的变量x便给出了问题的解答便给出了问题的解答因此因此:S=SA1 SA2 SBArtificialIntelligenceResolution:33 Graduate University , Chinese academy of Sciences. 谓词逻辑中的归结原理谓词逻辑中的归结原理置换与合一置换与合一归结式归结式归结反演归结反演ArtificialIntelligenceResolution:34 G
33、raduate University , Chinese academy of Sciences. 置换(Substitution)（1）例：例：C1：P(x) Q(x)C2：P(f(x) R(x)没有互补对没有互补对;例：例：C1：P(y) Q(y)y/xC1：P(f(x) Q(f(x)f(x)/yC3：R(x) Q(f(x)ArtificialIntelligenceResolution:35 Graduate University , Chinese academy of Sciences. 置换(2）置换和合一是为了处理谓词逻辑中子句之间的模式匹配而引进.定义: 置换是形如 t1/v1
34、,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)不是置换不是置换;ArtificialIntelligenceResolution:36 Graduate University , Chinese academy of Sciences. 置换-（3）定义： 不含任何元素的置换称为空置换，记为定义: 设=t1/v1,t2/v2, ,tn/vn是一个置换，E是一个表达式。将E中出现的每一个变量符号vi（1 i
35、n）,都用项ti置换，这样得到的表达式记为E ，称E 为E的例。ArtificialIntelligenceResolution:37 Graduate University , Chinese academy of Sciences. 置换-（4）例子：例子：E=P(x,y,z), =a/x,f(b)/y,c/zE =P(a,f(b),c)E=P(x,g(y),h(x,z), =a/x,f(b)/y,g(w)/zE =P(a,g(f(b),h(a,g(w)E=P(x,y,z), =y/x,z/yE =P(y,z,z).EP(z,z,z).(同时同时)ArtificialIntelligenc
36、eResolution:38 Graduate University , Chinese academy of Sciences. 置换的复合（乘积）（1）例子例子:E=P(x,y,z) =a/x,f(z)/y,w/zE =P(a,f(z),w) =t/z,g(b)/wE=P(a,f(t),g(b)=a/x,f(t)/y,g(b)/zArtificialIntelligenceResolution:39 Graduate University , Chinese academy of Sciences. 置换的复合（乘积）（2）定义： 设=t1/x1,t2/x2, ,tn/xn和 =u1/y1
37、,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所得的置换称为 和的复合或乘积,记为 ArtificialIntelligenceResolution:40 Graduate University , Chinese academy of Sciences. 置换的复合（乘积）-（3）定理：1.设和是两个置换,E是表达式，则 E ( )=(E ) 2.设,是三个置换,则有: 置换满足
38、结合率: ( ) = ( ) 置换的交换率不成立3. = = ArtificialIntelligenceResolution:41 Graduate University , Chinese academy of Sciences. 置换的复合（乘积）-（4） =a/x, =b/x=a/x=b/x ArtificialIntelligenceResolution:42 Graduate University , Chinese academy of Sciences. 合一（Unification）（1）定义: 设有公式集E=E1, . ,En和置换,使得:E1 = E2 = =En 则称E
39、1, . ,En是可合一的,并且称为一合一置换. 也称为 E1,En的合一子(unifier). 定义：如果对E1,En存在这样的合一子, 则称集合E1,En是可合一的.ArtificialIntelligenceResolution:43 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
40、(b) 1=a/x,f(b)/y(不唯一不唯一) 2=b/x,f(b)/yArtificialIntelligenceResolution:44 Graduate University , Chinese academy of Sciences. 最一般合一（1）定义:设是公式集E的一个合一,如果对于任一个合一,都存在置换使得: = , 则称是公式集E的最一般合一置换,记为mgu (most general unifier)ArtificialIntelligenceResolution:45 Graduate University , Chinese academy of Sciences.
41、 最一般合一（2）例子:E=P(x,y),P(x,f(b) 1=a/x,f(b)/y 2=b/x,f(b)/y =f(b)/y 1= a/x 2= b/xArtificialIntelligenceResolution:46 Graduate University , Chinese academy of Sciences. 差异集合 设W是非空表达式集合，W的差异集合D定义如下：首先找出W的所有表达式中不是都相同的第一个符号，然后从W的每个表达式中抽出占有这个符号位置的子表达式，所有这些子表达式组成的集合就是W的差异集合D。1.若D中无变量符号，则W是不可合一的2.若D中只有一个元素，则W是
42、不可合一的3.若D中的变量符号x和t，且x出现在t中，则W是不可合一的例子:W=P(x,f(y,z),z，w),P(x,a),P(x,g(z),z,b)D=f(y,z),a,g(z)ArtificialIntelligenceResolution:47 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)；否则
43、不可合一，停止(4)令 k+1= k tk /xk W k+1= W ktk /xk=W k+1(5) k=k+1 然后转(2)ArtificialIntelligenceResolution:48 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/yArtificialIntelligenceResolution:49 Graduate University , Chinese
44、 academy of Sciences. 合一算法（3）求W=P(a,x,f(g(y), P(z,f(z),f(u)的mgu.D0=a,z. 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)/uW3=W2 3=P(a,f(a),f(g(y) 3是是mgu.ArtificialIntelligenceResolution:50 Gradu
45、ate University , Chinese academy of Sciences. 合一算法（4）求W=Q(f(a), g(x), Q(y, y)的mgu.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.ArtificialIntelligenceResolution:51 Graduate University , Chinese academy of Sciences. 合一算法（5）求W=P(f(y), y), P(x, a)的mgu.D0=f(y),
46、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 =P(f(a),a) 2是mgu.ArtificialIntelligenceResolution:52 Graduate University , Chinese academy of Sciences. 合一算法（6）性质：1.若W是关于表达式的有限非空可合一集合，则合一算法将在第（2）步结束，并且最后的 k是W的mgu。2.若一组表达式E1, , En 是可合一的，则它们的mgu除
47、了相差一个改名外，是唯一确定。ArtificialIntelligenceResolution:53 Graduate University , Chinese academy of Sciences. 归结式归结式定义:设C1和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)ArtificialIntelligenceResolution:54 Gradua
48、te 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(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的的二元归结式二元归结式.ArtificialIntelligenceResolution:55 Graduate University , Chinese academy of
49、 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)ArtificialIntelligenceResolution:56 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
50、) Q(f(y)ArtificialIntelligenceResolution:57 Graduate University , Chinese academy of Sciences. 归结式定义:设C1和C2是无公共变量的子句,其归结式是下列二元归结式之一:(1) C1和C2的二元归结式(2) C1的因子和C2的二元归结式(3) C1和C2的因子的二元归结式(4) C1的因子和C2的因子的二元归结式该归结式仍记为R(C1,C2)ArtificialIntelligenceResolution:58 Graduate University , Chinese academy of Scie
51、nces. 归结式-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)ArtificialIntelligenceResolution:59 Graduate University , Chinese academy of Sciences. 归结反演设E为已知前提的公式集,Q为目标公式(或结论),用归结反演证明Q为真的步骤为:(1)否定Q得到Q(2)把Q加入到公式集E中,得到E, Q(3)把公式集E, Q化为子句集S(4)应用归结原理
52、对子句集S中的子句进行归结,并把每次归结所得的归结式并入S中.如此反复进行,若出现空子句,则停止归结,此时就证明了Q为真.ArtificialIntelligenceResolution:60 Graduate University , Chinese academy of Sciences. 归结反演示例一 已知：求证： ArtificialIntelligenceResolution:61 Graduate University , Chinese academy of Sciences. 归结反演示例二给定下面一段话： Tony、Mike和 John都是Alpine Club的会员。每个
53、会员或者是一个滑雪爱好者，或者是一个登山爱好者，或者都是。没有一个登山爱好者喜欢下雨，所有的滑雪爱好者都喜欢雪。 Tony喜欢的所有东西 Mike都不喜欢， Tony不喜欢的所有东西 Mike都喜欢。 Tony喜欢雨和雪。 用谓词演算表达上述信息。把问题“谁是该俱乐部的会员，他是一个登山爱好者，但不是滑雪爱好者”表达为一个谓词表达式，用归结反驳提取答案ArtificialIntelligenceResolution:62 Graduate University , Chinese academy of Sciences. 归结的完备性问题的提出：若定理成立，是否使用归结方法必能得到证明？或者说
54、：使用归结方法推出的定理的个数和所有成立的定理的个数是否一样多？ArtificialIntelligenceResolution:63 Graduate University , Chinese academy of Sciences. Herbrand定理定理由来由来为了评定子句集的不可满足性为了评定子句集的不可满足性,就需要对子句集中的子句就需要对子句集中的子句进行评定进行评定.一般情况下一般情况下,要评定一个子句的不可满足性要评定一个子句的不可满足性,需需要对个体域上的一切解释逐个地进行评定要对个体域上的一切解释逐个地进行评定.但是由于个体但是由于个体变量论域的任意性变量论域的任意性,以
55、及解释个数的无限性以及解释个数的无限性,因此评定子因此评定子句集的不可满足性是很困难的句集的不可满足性是很困难的.Herbrand域就是一个特殊的域域就是一个特殊的域,只要在这个论域上公式只要在这个论域上公式不可满足不可满足,则该公式就在任一论域上也不可满足则该公式就在任一论域上也不可满足ArtificialIntelligenceResolution:64 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H域域定义定义:设设S为子句集为子句集,则按下述方法构造的域则按下述方法构造的域H 称为称为H域域:(1)令令
56、H0是是S中所有的个体常量的集合中所有的个体常量的集合,若若S中不包含个体常中不包含个体常量量,则任取常量则任取常量a D,而规定而规定H0=a(2)令令Hi+1=Hi 所有形如所有形如f(t1,tn)的元素的元素其中其中:f(t1,tn)是出现于是出现于S中的任一函数中的任一函数,而而t1,tn是是Hi中的元素中的元素.i=1,2,.H域是直接依赖于域是直接依赖于S的最多只有可数个元素的最多只有可数个元素ArtificialIntelligenceResolution:65 Graduate University , Chinese academy of Sciences. Herbrand
57、定理定理-H域域例一例一:S=P(a),P(x) P(f(x)根据定义有根据定义有:H0=aH1=a f(a)=a,f(a)H2=a,f(a) f(a),f(f(a)=a,f(a),f(f(a)H =a,f(a),f(f(a),.例二例二:S=P(x),Q(y) R(z)H0=H1=H =aArtificialIntelligenceResolution:66 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H域域例三：例三：S=P(f(x)，a，g(y)，b)H0=a，bH1=a，b，f(a)，g(a)，f(b)
58、，g(b)H2=a，b，f(a)，g(a)，f(b)，g(b)，f(f(a)，f(g(a)，f(f(b)，f(g(b)，g(f(a)，g(g(a)，g(f(b)，g(g(b).ArtificialIntelligenceResolution:67 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H域域基础基础(ground)/基基没有变量的项称为基础项没有变量的项称为基础项(groundterm).f(a,b)没有变量的原子称为基础原子没有变量的原子称为基础原子(groundatom).P(a,f(b)没有变量的文
59、字称为基础文字没有变量的文字称为基础文字(groundliteral).P(a,f(b),P(a,f(b)没有变量的子句称为基础子句没有变量的子句称为基础子句(groundclause).P(b,f(b) Q(f(f(b)ArtificialIntelligenceResolution:68 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H域域原子集原子集:子句中所有基原子构成的集合称为原子集子句中所有基原子构成的集合称为原子集.令令S是一个子句集合是一个子句集合,形如形如P(t1,.,tn)的基础原子集合的基础
60、原子集合,称为称为S的原子集的原子集.记为记为A.其中其中,P(t1,.,tn)是出现在是出现在S中的任一谓词符号中的任一谓词符号,而而t1,.,tn是是S的的H域的任意元素。域的任意元素。ArtificialIntelligenceResolution:69 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H域域S=P(z),P(x) Q(y)H=aA=P(a),Q(a)S=P(a),P(x) P(f(x)H=a,f(a),f(f(a),.A=P(a),P(f(a),P(f(f(a),.S=P(f(x),a,g(
61、y),b)H=a,b,f(a),g(a),f(b),g(b),A=P(a,a,a,a),P(a,a,a,b),P(a,a,b,b),.ArtificialIntelligenceResolution:70 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H域域定义定义(基础实例基础实例)当当S中的某子句中的某子句C中所有变量符号均以中所有变量符号均以S的的H域的元素代域的元素代入时，所得的基子句入时，所得的基子句C称作称作C的一个基础实例的一个基础实例(基例）基例）例例S=P(x),Q(f(y) R(y),Z(f(
62、y)H=a,f(a),f(f(a),.P(a),P(f(a)都称作子句都称作子句C=P(x)的基例。的基例。同样同样,Q(f(a) R(a),Q(f(f(a) R(f(a)都是都是Q(f(y) R(y)的基例。的基例。Q(a) R(a)不是不是Q(f(y) R(y)的基例。的基例。对于任一对于任一b D,子句子句P(b),Q(f(b) R(b)都叫基子句。都叫基子句。ArtificialIntelligenceResolution:71 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H的解释的解释起因起因由子句集
63、由子句集S建立建立H域、原子集域、原子集A;一般论域一般论域D上对上对S的解释的解释IH域上的解释域上的解释I*;S在在D上为真上为真 S在在H上为真上为真;S在在D上不可满足上不可满足 S在在H上不可满足上不可满足; ArtificialIntelligenceResolution:72 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H的解释的解释H解释的表示解释的表示令令A=A1,An,是是S的原子集的原子集,一个一个H解释可被表示为解释可被表示为:I=m1,mn,其中其中mj或者是或者是Aj或者是或者是Aj
64、.如果如果mj是是Aj,则则Aj为真为真,否则否则,Aj为假为假.ArtificialIntelligenceResolution:73 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H的解释的解释定义定义:子句集子句集S在在H域上的一个解释域上的一个解释I*满足下列条件满足下列条件:(1)在解释在解释I*下下,常量映射到自身常量映射到自身(2)S中的任一中的任一n元函数是元函数是HnH的映射的映射.即假设即假设h1,h2,hn H,则则f(h1,h2,hn) H(3)S中的任一个中的任一个n元谓词是元谓词是Hn
65、T,F的映射的映射.ArtificialIntelligenceResolution:74 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H的解释的解释例子例子:S=P(x) Q(x),R(f(y)H=a,f(a),f(f(a),.A=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),S的的H解释解释,如如:I*1=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),I*2=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),I*3=P(a),Q(a)
66、,R(a),P(f(a),Q(f(a),R(f(a),则有则有:S|I*1=T,S|I*2=F,S|I*3=FArtificialIntelligenceResolution:75 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H的解释的解释由由S在在D域的解释域的解释I如何确定相应的如何确定相应的S在在H域的解释域的解释I*:(1)若若S中有常量符号中有常量符号,任一任一a H0,在在I下下a取值为取值为a0,就规定就规定aa0(2)若若S中无常量符号中无常量符号,H0=a,就规定就规定aa0,a0是是D的任一
67、元素的任一元素(3)若若f(hf(h1 1,h,h2 2, , ,h ,hn n) )是是S S中的任一函数符号中的任一函数符号, ,任取任取(h(h1 1,h,h2 2, , ,h,hn n ) ) H Hn ni i. .当在当在I I下下(h(h1 1,h,h2 2, , ,h ,hn n) )取值为取值为(h(h0 01 1,h,h0 02 2, , ,h,h0 0n n),),且在且在I I下对应值为下对应值为f (hf (h0 01 1,h,h0 02 2, , ,h ,h0 0n n)()(为为D D中的元素中的元素),),就规定就规定: : f(h f(h1 1,h,h2 2,
68、 , ,h ,hn n) ) f (hf (h0 01 1,h,h0 02 2, , ,h ,h0 0n n) )则则I*是如下的是如下的H解释：解释：VI*(P(h h1 1,h,h2 2, , ,h ,hn n)=VI(P(h h0 01 1,h,h0 02 2, ,h,h0 0n n)ArtificialIntelligenceResolution:76 Graduate University , Chinese academy of Sciences. Herbrand定理定理-H的解释的解释定理定理:设设I是是S的论域的论域D上的解释上的解释,存在对应于存在对应于I的的H解释解释I*
69、,使得如使得如果果S|I=T,则有则有S|I*=T定理定理:子句集子句集S是不可满足的是不可满足的,当且仅当在所有的当且仅当在所有的S的的H解释下为解释下为假假()设设S是不可满足的是不可满足的.则在任一个论域上的任一解释使则在任一个论域上的任一解释使S为假为假;H是一个论域是一个论域;()设设S的所有的的所有的H解释使解释使S为假为假.假设子句集假设子句集S可满足可满足.在某个论域上的某个解释在某个论域上的某个解释I使使S为真为真;I在在H域上对应解释域上对应解释I*;根据引理，根据引理，I*满足满足S.ArtificialIntelligenceResolution:77 Graduate
70、 University , Chinese academy of Sciences. Herbrand定理定理-语义树语义树语义树是通过将语义树是通过将S的所有解释展示在一棵树上的所有解释展示在一棵树上,从几何上对从几何上对S的不可满足性的不可满足性进行讨论进行讨论Example1G=P Q RS=P,Q,RA=P,Q,RPPQQQQRRRRRRRRArtificialIntelligenceResolution:78 Graduate University , Chinese academy of Sciences. Herbrand定理定理-语义树语义树Example2S=P(x) Q(x
71、),P(f(y),Q(f(y)H=a,f(a),f(f(a),.A=P(a),Q(a),P(f(a),Q(f(a),.P(a)P(a)Q(a)Q(a)Q(a)Q(a)P(f(a) P(f(a)P(f(a) P(f(a)P(f(a) P(f(a). ArtificialIntelligenceResolution:79 Graduate University , Chinese academy of Sciences. Herbrand定理定理-语义树语义树颠颠倒倒原原子子的的顺顺序序是是可可以以的的.例例如如Q(a)为为第第一一个个顶顶点点.如如果果原原子子集集是是无无限限的的，则则对对应应的
72、的语语义义树树必必定定是是无无限限的的.从任一个叶节点向根节点看从任一个叶节点向根节点看, 代表代表S的一个解释的一个解释.从从任任一一个个中中间间节节点点向向根根节节点点看看, 代代表表S的的一一个个部部分分解释解释.ArtificialIntelligenceResolution:80 Graduate University , Chinese academy of Sciences. Herbrand定理定理-语义树语义树语义树的特点语义树的特点:S的语义树是完全的的语义树是完全的,如果如果N表示叶节点表示叶节点,则则I(N)包包含了含了S的原子集中所有元素或者该元素的否定的原子集中所有
73、元素或者该元素的否定语义树每个直到叶节点的分枝都对应于语义树每个直到叶节点的分枝都对应于S的一个的一个解释解释.特别对有限树来说特别对有限树来说,I(N)就是就是S的一个解释的一个解释如果节点如果节点N的的I(N)使使S的某一子句的某一集子句为的某一子句的某一集子句为假假,而而N的父辈节点不能评定这个事实的父辈节点不能评定这个事实,则称则称N为为失败节点失败节点如果如果S的完全语义树的每个分枝上都有一个失败的完全语义树的每个分枝上都有一个失败节点节点,就说该语义树为封闭语义树就说该语义树为封闭语义树ArtificialIntelligenceResolution:81 Graduate Uni
74、versity , Chinese academy of Sciences. Herbrand定理定理-语义树语义树ExampleS=P,Q R,P Q,P RPPQQQQRRRRRRRRArtificialIntelligenceResolution:82 Graduate University , Chinese academy of Sciences. Herbrand定理定理-语义树语义树封闭语义树：封闭语义树：PPQQRRArtificialIntelligenceResolution:83 Graduate University , Chinese academy of Scien
75、ces. Herbrand定理定理-语义树语义树ExampleS=P(x),P(x) Q(f(x),Q(f(a)A=P(a),Q(a),P(f(a),Q(f(a),P(a)Q(f(a)P(a)Q(f(a)ArtificialIntelligenceResolution:84 Graduate University , Chinese academy of Sciences. Herbrand定理定理-语义树语义树证明一个定理就是寻找一棵封闭语义树证明一个定理就是寻找一棵封闭语义树.S不可满足不可满足S在所有解释下为假在所有解释下为假S在所有在所有H解释下为假解释下为假;完备语义树包含所有完备语
76、义树包含所有H解释解释;每一枝是一个每一枝是一个H解释解释;S在在I下为假下为假,则使某个基础实例为假则使某个基础实例为假;这个节点称为假节点这个节点称为假节点,不用再扩展不用再扩展;所有枝上都有假节点所有枝上都有假节点,则为封闭语义树则为封闭语义树;ArtificialIntelligenceResolution:85 Graduate University , Chinese academy of Sciences. Herbrand定理定理Herbrand定理定理(1):子句集子句集S是不可满足的是不可满足的,当且仅当对应于当且仅当对应于S的的完全语义树都是一棵有限封闭语义树完全语义树都
77、是一棵有限封闭语义树ArtificialIntelligenceResolution:86 Graduate University , Chinese academy of Sciences. Herbrand定理定理Herbrand定理定理(2):子句集子句集S是不可满足的是不可满足的,当且仅当存在不可满足的当且仅当存在不可满足的S的有限基例的有限基例集集S例子例子:S=P(x),P(a) P(b),Q(f(x)H=a,b,f(a),f(b),f(f(a),f(f(b)A=P(a),P(b),Q(a),Q(b),S=P(a),P(b),P(a) P(b)P(a)P(b)P(a)P(b)Art
78、ificialIntelligenceResolution:87 Graduate University , Chinese academy of Sciences. 困难生成基础实例集合是指数复杂性的例子: S=P(x,g(x),y,h(x,y),z,k(x,y,z), P(u,v,e(v),w,f(v,w),x)H0=aH1=a,g(a),h(a,a),k(a,a,a),e(a),f(a,a)基础实例集：S0= P(a,g(a),a,h(a,a),a,k(a,a,a), P(a,a,e(a),a,f(a,a),a)S1有6*6*6 + 6*6*6*6 = 1512个元素;H5有1064数量
79、级的元素，S5有10256数量级的元素. ArtificialIntelligenceResolution:88 Graduate University , Chinese academy of Sciences. 一些简化计算规则(1)重言式子句可删除规则重言式子句可删除规则S中的重言式子句，不会为中的重言式子句，不会为S的不可满足提供任的不可满足提供任何信息，可以删除何信息，可以删除S=P P，Q，R PS的逻辑含义是的逻辑含义是（P P） Q (R P)=Q (R P)，从而删去重言式从而删去重言式P P，不影响不影响S的真值。的真值。S=Q，R PArtificialIntellige
80、nceResolution:89 Graduate University , Chinese academy of Sciences. 一些简化计算规则(2)单文字删除规则单文字删除规则单文字单文字:在在S中存在只有一个文字的基础子句中存在只有一个文字的基础子句L.如如S=L,L C1,L C2,C3,C4,其中其中C3,C4不含不含L和和L.从从S中删除含中删除含L的子句得到的子句得到:S=L C2,C3,C4从从S中删除文字中删除文字L得到得到:S =C2,C3,C4若若S为空为空,则则S是可满足的是可满足的若若S不空不空,则则S和和S 同时是不可满足的同时是不可满足的.Artificia
81、lIntelligenceResolution:90 Graduate University , Chinese academy of Sciences. 一些简化计算规则(3)纯文字删除规则纯文字删除规则定义定义:当文字当文字L出现于出现于S中中,而而L不出现于不出现于S中时中时,则称则称L为为S的纯文字的纯文字从从S中删除含中删除含L的子句得的子句得S.如果如果S为空集为空集,则则S是可满足的是可满足的如果如果S非空非空,则则S与与S同时是不可满足的同时是不可满足的例子例子:S=A B,A B,B,BS=B,B;ArtificialIntelligenceResolution:91 Gra
82、duate University , Chinese academy of Sciences. 一些简化计算规则(4)分离规则分离规则若若S=(L A1) (L Am) (L B1) (L Bn) R其中其中R是不含是不含L和和L的文字集的文字集令令S=A1,.,Am,RS =(B1,Bn,R则则S不可满足当且仅当不可满足当且仅当S和同时不可满足和同时不可满足S ArtificialIntelligenceResolution:92 Graduate University , Chinese academy of Sciences. 一些简化计算规则(5)S=P Q R,P Q,P,R,U对对
83、U使用纯文字使用纯文字:P Q R,P Q,P,R对对P使用单文字使用单文字:Q R,Q,R对对Q使用单文字使用单文字:R,R对对R使用单文字使用单文字: S不可满足不可满足;S=P Q,Q,P Q R对对Q使用单文字使用单文字:P,P R对对P使用单文字使用单文字:R对对R使用纯文字使用纯文字:S可满足；可满足；ArtificialIntelligenceResolution:93 Graduate University , Chinese academy of Sciences. 归结和语义树“倒塌”过程例：S=P, PQ, P Q A=P,Q归结过程：(1) P (2) P Q(3) P
84、 Q (4) P (2)(3) (5) (1)(4)PQN11N12N21N24TN0PQN11N12N21T*N0PN11T(1)ArtificialIntelligenceResolution:94 Graduate University , Chinese academy of Sciences. 归结的完备性提升引理提升引理:C1、C2是无公共变量的子句，而是无公共变量的子句，而C1、C2分别是分别是C1、C2的例，的例，R是是C1、C2的归结式，则存在的归结式，则存在C1、C2的归结式的归结式R，使得使得R是是R的例的例ArtificialIntelligenceResolution
85、:95 Graduate University , Chinese academy of Sciences. 归结的完备性例子C1:P(x) Q(f(x)C2:Q(y) R(y)C1:P(a) Q(f(a)a/xC2:Q(f(a) R(f(a)f(a)/yC:P(a) R(f(a)C:P(x) R(f(x)ArtificialIntelligenceResolution:96 Graduate University , Chinese academy of Sciences. 归结的完备性完备性定理：完备性定理：S是不可满足的当且仅当存在一个使用归结推理规是不可满足的当且仅当存在一个使用归结推
86、理规则的从则的从S到空子句到空子句 的推理过程的推理过程ArtificialIntelligenceResolution:97 Graduate University , Chinese academy of Sciences. 效率的问题（效率的问题（1）归结原理比Herbrand定理有了明显的进步;盲目的归结会产生组合爆炸问题;不必要的归结式 不必要的归结式;ArtificialIntelligenceResolution:98 Graduate University , Chinese academy of Sciences. 效率的问题（效率的问题（2）S=P Q,P Q,P Q,P
87、Q盲目归结过程盲目归结过程:S0=SSi=C1,C2的归结式的归结式|C1 S0 S1 Si-1,C2 Si-1具体过程具体过程:S0:(1)P Q(2)P Q(3)P Q(4)P QS1:(5)Q(1)(2)(6)P(1)(3)(7)Q Q(1)(4)(8)P P(1)(4).(12)QS2:(13)P Q(1)(7)(14)P Q(1)(8).(39)nil(5)(12)ArtificialIntelligenceResolution:99 Graduate University , Chinese academy of Sciences. Agenda引言引言命题逻辑中的归结原理命题逻辑
88、中的归结原理谓词逻辑中的归结原理谓词逻辑中的归结原理非单调推理非单调推理ArtificialIntelligenceResolution:100 Graduate University , Chinese academy of Sciences. 非单调推理非单调推理什么是非单调推理什么是非单调推理主要的非单调逻辑主要的非单调逻辑封闭世界假设封闭世界假设(CWA)限制理论限制理论缺省逻辑缺省逻辑ArtificialIntelligenceResolution:101 Graduate University , Chinese academy of Sciences. 什么是非单调推理什么是非单
89、调推理(1)科学的发现过程是一个科学的发现过程是一个证伪证伪的过程，人类知识的增长是一个非单调的过的过程，人类知识的增长是一个非单调的过程程传统的逻辑系统实际上作的是单调推理，加进系统的新知识（信念）必传统的逻辑系统实际上作的是单调推理，加进系统的新知识（信念）必须与已有的知识（信念）相一致，不会引起矛盾。所以，随着运行时间须与已有的知识（信念）相一致，不会引起矛盾。所以，随着运行时间的推移，系统内含的知识有增无减，这就是所谓的单调性。的推移，系统内含的知识有增无减，这就是所谓的单调性。 设设FSFS为一个逻辑系统，如果对于为一个逻辑系统，如果对于FSFS的任意两个公式的任意两个公式集合集合T
90、 T和和S S，T T是是S S的子集，则的子集，则Th(TTh(T) )也是也是Th(STh(S) ) 的子集的子集 ( (Th(TTh(T) ) 表示从表示从T T中推出的定理中推出的定理的集合的集合=A|TA|TA A)这说明向一个公理理论中增加新的定理不会影响该理论已经有的定理，这说明向一个公理理论中增加新的定理不会影响该理论已经有的定理，初始理论原来已经有的定理仍然是扩大了以后理论的定理。初始理论原来已经有的定理仍然是扩大了以后理论的定理。 ArtificialIntelligenceResolution:102 Graduate University , Chinese acade
91、my of Sciences. 什么是非单调推理什么是非单调推理(2)单调性的优点在于：单调性的优点在于： （1）加加入入新新命命题题时时不不需需审审查查与与系系统统原原有有知知识识的的相相容容性性，因因为为这这些些新新命命题题只只能能是是已已有有知知识识的的逻逻辑辑推推理理结结果果，不不可能引起矛盾。换言之，加入的新命题必定是永真的。可能引起矛盾。换言之，加入的新命题必定是永真的。 （2）不不需需要要记记忆忆推推导导过过程程。因因为为推推导导的的结结论论永永远远不不会失败，不存在事后审查推导过程的需求问题。会失败，不存在事后审查推导过程的需求问题。ArtificialIntelligence
92、Resolution:103 Graduate University , Chinese academy of Sciences. 什么是非单调推理什么是非单调推理(3)非单调性推理非单调性推理推理系统的定理集合并不随推理过程的进行而增大，新推理系统的定理集合并不随推理过程的进行而增大，新推出的定理很可能会否定、改变原来的一些定理。推出的定理很可能会否定、改变原来的一些定理。推理时所依据的推理时所依据的知识具有不完全性知识具有不完全性 逻辑系统是非单调的，如果存在公式集合逻辑系统是非单调的，如果存在公式集合T T和和S S，如果如果T T S S，但但Th(T)Th(T) Th(STh(S)
93、)ArtificialIntelligenceResolution:104 Graduate University , Chinese academy of Sciences. 什么是非单调推理什么是非单调推理(4)需要非单调推理的理由主要为：需要非单调推理的理由主要为：知识的不完全知识的不完全 一个有限的信念集合仅仅是现实世界的近似描述，会有一个有限的信念集合仅仅是现实世界的近似描述，会有很多的例外很多的例外-资格问题资格问题 客观世界变化太快，一个不断变化的世界必须用变化的客观世界变化太快，一个不断变化的世界必须用变化的知识库加以描述知识库加以描述 框架问题框架问题非单调推理比单调推理难处
94、理得多。因为当一个假设被发现非单调推理比单调推理难处理得多。因为当一个假设被发现错误而撤消时，一系列基于它的推理结果都要撤消。所以，错误而撤消时，一系列基于它的推理结果都要撤消。所以，设计非单调推理系统的一个关键问题在于防止系统花费过多设计非单调推理系统的一个关键问题在于防止系统花费过多的时间在这种处理上。的时间在这种处理上。 ArtificialIntelligenceResolution:105 Graduate University , Chinese academy of Sciences. 什么是非单调推理什么是非单调推理(5)非单调推理的研究有两条途径：非单调推理的研究有两条途径：
95、对逻辑的扩展：这涉及非单调推理的形式化方面，称为非单对逻辑的扩展：这涉及非单调推理的形式化方面，称为非单调逻辑，它包括：语言方面的扩充（指增强其表达能力）和调逻辑，它包括：语言方面的扩充（指增强其表达能力）和语义方面的扩充（指对真值的真假两种情况进行修正）；主语义方面的扩充（指对真值的真假两种情况进行修正）；主要包括：要包括：基基于于最最小小化化语语义义：主主要要有有封封闭闭世世界界假假设设、McCarthy的的限限制制逻逻辑辑（circumscription）、）、Konolige的忽略逻辑等的忽略逻辑等基基 于于 定定 点点 定定 义义 ： 主主 要要 有有 缺缺 省省 逻逻 辑辑 (de
96、fault)和和 自自 认认 知知 逻逻 辑辑(autoepistemic)等。等。 对推理模式的扩展：这涉及非单调推理的过程化方面，称为对推理模式的扩展：这涉及非单调推理的过程化方面，称为非单调系统。这可以通过对矛盾的检测进行真值的修正来维非单调系统。这可以通过对矛盾的检测进行真值的修正来维护相容性，可称为真值维护系统。护相容性，可称为真值维护系统。ArtificialIntelligenceResolution:106 Graduate University , Chinese academy of Sciences. 什么是非单调推理什么是非单调推理(6)非单调推理的三个主要流派：非单调
97、推理的三个主要流派：1.McCarthy的限制理论：当且仅当没有事实证明的限制理论：当且仅当没有事实证明S在更在更大的范围成立时，大的范围成立时，S只在指定的范围成立；只在指定的范围成立；2.Reiter的缺省逻辑：的缺省逻辑：“S在缺省的条件下成立在缺省的条件下成立”是指是指“当且仅当没有事实证明当且仅当没有事实证明S不成立时不成立时S是成立的是成立的”。3.Moore的自认知逻辑：的自认知逻辑：“如果我知道如果我知道S，并且我不知道并且我不知道有其他任何事实与有其他任何事实与S矛盾，则矛盾，则S是成立的是成立的”。ArtificialIntelligenceResolution:107 G
98、raduate University , Chinese academy of Sciences. 封闭世界假设封闭世界假设(1)(1)在非单调领域中的推理，我们必须给出下面的假设：在非单调领域中的推理，我们必须给出下面的假设：封闭世界假设（封闭世界假设（ClosedWorldAssumption:CWA），），或者或者增加新的事实，继续推理增加新的事实，继续推理封闭世界假设是一种对由一组基本信念集合封闭世界假设是一种对由一组基本信念集合KBKB定义的理论定义的理论T(KB)T(KB)进行完进行完备化的方法。备化的方法。我们说一个理论我们说一个理论T(KB)T(KB)是完备的，是说其包含（显式
99、或隐含）了每一是完备的，是说其包含（显式或隐含）了每一个基原子公式或该公式否定。个基原子公式或该公式否定。CWAWA的基本思想是：如果无法证明的基本思想是：如果无法证明P P，则就认为它是否定的。即：则就认为它是否定的。即：如果从知识库中无法证明如果从知识库中无法证明P P或者或者 P P，则就向则就向KBKB中增加中增加 P P即假定知道所有有关世界的事情（世界是封闭的）即假定知道所有有关世界的事情（世界是封闭的）ArtificialIntelligenceResolution:108 Graduate University , Chinese academy of Sciences. 封闭
100、世界假设封闭世界假设(2)(2)CWACWA是非单调的：是非单调的：CWA对理论的完备化是仅仅通过向基本信念集合对理论的完备化是仅仅通过向基本信念集合KB中增加基原子公中增加基原子公式的取反来实现的。式的取反来实现的。一旦以后有新的基原子公式加进一旦以后有新的基原子公式加进KBKB，则为完备则为完备T T（KBKB）而生成的扩充而生成的扩充集就必须收缩（删除该基原子公式的否定）。集就必须收缩（删除该基原子公式的否定）。 由于为完备由于为完备T(KB)T(KB)而生成的扩充集中的每个基原子公式的取反均是假设而生成的扩充集中的每个基原子公式的取反均是假设的暂时信念，记该扩充集为的暂时信念，记该扩充
101、集为KBKBasmasm。对于一个基原子公式对于一个基原子公式P P，CWACWA可可定义：定义： P P KBKBasmasm，当且仅当当且仅当P P T(KB) T(KB)。经经过过由由CWACWA方方法法完完备备的的理理论论为为CWA(KB),CWA(KB),它它扩扩大大了了T(KB)T(KB)的的推推理理能能力力, ,允允许许不能由不能由KBKB导出的结论可以由导出的结论可以由KBKB KBKBasmasm导出导出. .ArtificialIntelligenceResolution:109 Graduate University , Chinese academy of Scienc
102、es. 封闭世界假设封闭世界假设(3)(3)CWACWA方法并不确保被完备的理论方法并不确保被完备的理论CWA(KB)CWA(KB)是一致的，解决不一致性是非单是一致的，解决不一致性是非单调推理的重要议题，需要对调推理的重要议题，需要对CWACWA的完备性规则进行修改，以实现一致性。的完备性规则进行修改，以实现一致性。CWA(KB)CWA(KB)是一致的，当且仅当对于每个可由是一致的，当且仅当对于每个可由KBKB推导出的子句推导出的子句P P1 1 P P2 2 P Pn n，都至少存在一个都至少存在一个P Pi i可从可从KBKB推导出；其中推导出；其中P Pi i均为正基文字。均为正基文字
103、。若若KBKB是由一致的是由一致的HornHorn形子句组成时，则形子句组成时，则CWA(KB)CWA(KB)必定一致必定一致 ArtificialIntelligenceResolution:110 Graduate University , Chinese academy of Sciences. 限制理论限制理论（1）限制理论的核心思想是：限制理论的核心思想是：如果一个句子叙述一个命题，那么它叙述的仅仅是这个命题，如果一个句子叙述一个命题，那么它叙述的仅仅是这个命题，一点都不能扩张和延伸，任何多余的东西都要删除掉。一点都不能扩张和延伸，任何多余的东西都要删除掉。这就是所谓的这就是所谓的“
104、OccamOccam剃刀原理剃刀原理”，McCarthyMcCarthy称为极小模型。称为极小模型。限制理论最初是用于定义通常什么事物是成立的这可以在FOL中定义一个”尽可能错”的特殊异常的谓词：ab然后通过最小化ab的扩展，最小化该异常性即除了那些已知为真的对象外，其他都为假ArtificialIntelligenceResolution:111 Graduate University , Chinese academy of Sciences. 限制理论限制理论（2）and_gate(x, in1, in2, out) zero(in1) ab(x) zero(out)block(x) a
105、b(x) on table(x)holds(F, t) ab(F, t + 1) holds(F, t + 1)ArtificialIntelligenceResolution:112 Graduate University , Chinese academy of Sciences. 限制理论限制理论（3）限制有多种形式，如：平行限制（公式限制）论域限制谓词限制ArtificialIntelligenceResolution:113 Graduate University , Chinese academy of Sciences. 平行限制p限制作为二阶公式：限制作为二阶公式：令 P =
106、Q 表示 x(P(x) Q(x)令 P Q 表示 x(P(x) Q(x)令 P Q 表示 (P Q) (P = Q)令 A(P) 表示包含谓词P的句子pA中P的限制CIRC(A; P)为： A(P) qA(q) q P直觉上看：P是使得A为真的最小的谓词之一。ArtificialIntelligenceResolution:114 Graduate University , Chinese academy of Sciences. 论域限制论域限制论域限制的含义是：论域限制的含义是：只有那些存在的事物才是已知的，未知的事物都是不知道的。只有那些存在的事物才是已知的，未知的事物都是不知道的。设设
107、 为一阶公式，设个体域为为一阶公式，设个体域为 x x | | P(P(x x)，A为一个命题，为一个命题， ( (x x) )为带有为带有自由变量自由变量x x的一阶公式，令：的一阶公式，令： A = = A x x( ( ( (x x) )B(B(x x)/)/ xBxB( (x x) )， x x( ( ( (x x) ) B(B(x x) /) / x x B(B(x x)则对则对A中的中的P P做限制为：做限制为： A x x( ( ( (x x)这称为这称为A的论域限制。的论域限制。域限制是针对一个谓词的外延做出的域限制是针对一个谓词的外延做出的ArtificialIntellig
108、enceResolution:115 Graduate University , Chinese academy of Sciences. 谓词限制谓词限制谓词限制：从个体所具有的性质角度来讨论谓词限制：从个体所具有的性质角度来讨论定义：定义： 设设A A是包含谓词是包含谓词P(x1,x2,.,xn)P(x1,x2,.,xn)的一阶逻辑句子，其中的一阶逻辑句子，其中P(x1,x2,.,xn)P(x1,x2,.,xn)可简记可简记P(P(x x x x),),则则P P在在 (P)(P)中的限制为如下的中的限制为如下的公式模式：公式模式： ( ( ) )x x x x( ( ( (x x x x
109、) ) P P( (x x x x) x x x x(P(P(x x x x) ) ( (x x x x)其中：其中： (P)(P)表示表示A A中的谓词中的谓词P P， ( ( ) )表将表将 中所有中所有P P的出现换的出现换为公式为公式 后的结果后的结果ArtificialIntelligenceResolution:116 Graduate University , Chinese academy of Sciences. 缺省逻辑缺省逻辑（1）缺省推理（也称为默认逻辑）是在信息不完全和前提缺省的情况下，默缺省推理（也称为默认逻辑）是在信息不完全和前提缺省的情况下，默认一些先决条件而进
110、行的推理。认一些先决条件而进行的推理。基本思想是：传统的逻辑是从已知的事实推出新的事实，在推理时，知基本思想是：传统的逻辑是从已知的事实推出新的事实，在推理时，知识库的丰富程度决定了能推出多少事实。而在非单调推理中，知识库不识库的丰富程度决定了能推出多少事实。而在非单调推理中，知识库不够丰富，难以支持系统所需要的推理，因此需要对知识库进行扩充，这够丰富，难以支持系统所需要的推理，因此需要对知识库进行扩充，这些扩充的知识就是缺省的知识。些扩充的知识就是缺省的知识。 ReiterReiter的缺省逻辑包括一阶的语句以及一个或多个缺省假设。的缺省逻辑包括一阶的语句以及一个或多个缺省假设。形形式式地地
111、说说，缺缺省省逻逻辑辑DLDL是是对对基基本本的的知知识识库库KBKB扩扩充充一一组组非非标标准准的的、非非单单调调的的推推理理规规则则D D实实现现的的。扩扩充充了了D D的的KBKB包包括括标标准准逻逻辑辑所所具具有有的的结结论论加加上上应应用用D D于于KBKB所得到的结论。所得到的结论。 ArtificialIntelligenceResolution:117 Graduate University , Chinese academy of Sciences. 缺省逻辑缺省逻辑（2）DL系统系统D中的缺省规则形式为：中的缺省规则形式为：或者表示为线性形式为：或者表示为线性形式为：M为为
112、缺缺省省算算子子，表表示示相相容容性性，即即前前提提和和缺缺省省条条件件相相容容或或不不矛矛盾盾，就就可可以以推出结论。推出结论。ArtificialIntelligenceResolution:118 Graduate University , Chinese academy of Sciences. 缺省逻辑缺省逻辑（3）如如果果缺缺省省规规则则中中不不含含有有自自由由变变元元，即即 、M i、W都都是是命命题题，那那么么该该规规则称为闭规则。则称为闭规则。一个缺省理论一个缺省理论T由两个部分组成：由两个部分组成：1、缺省推理规则集合缺省推理规则集合D2、公式集合公式集合W，它是已知的或约
113、定的事实的集合它是已知的或约定的事实的集合当当D中所有规则都是闭规则时，称理论中所有规则都是闭规则时，称理论T=为闭缺省理论为闭缺省理论ArtificialIntelligenceResolution:119 Graduate University , Chinese academy of Sciences. 例例假设假设W为：为：bird(tweety) x(ostrich(x) flies(x) D为：为： 则可以得到则可以得到flies(tweety)。 如果在如果在W中增加中增加ostrich(tweety)，则无法得到则无法得到flies(tweety)。ArtificialInte
114、lligenceResolution:120 Graduate University , Chinese academy of Sciences. 缺省逻辑（4）在在缺缺省省理理论论中中，“推推出出”概概念念和和传传统统逻逻辑辑中中的的“推推出出”概概念念是是有有区区别别的的，前者是非单调推理而后者是单调推理。前者是非单调推理而后者是单调推理。设设 =为为一一闭闭缺缺省省理理论论， 为为关关于于D的的一一个个算算子子， 作作用用于于任任意意的的命题集合命题集合S，其值为满足下面三个性质的最小命题集合其值为满足下面三个性质的最小命题集合 (S):(1)W (S)；(2) (S)为在普通命题演算的
115、推理下封闭的，即为在普通命题演算的推理下封闭的，即Th( (S)= (S)；(3)如果如果D中有规则：中有规则：且且(S)，1,m S，那么那么w(S)。ArtificialIntelligenceResolution:121 Graduate University , Chinese academy of Sciences. 缺省逻辑（5）命命题题集集合合E称称为为关关于于D的的算算子子 的的固固定定点点，如如果果 (E)=E。此此时时又又称称E为为 =的一个扩张。的一个扩张。如如果果命命题题A包包含含在在缺缺省省理理论论 =的的一一个个扩扩张张中中，那那么么称称A在在 中中可以推出，记为可
116、以推出，记为|，表示非单调，表示非单调“推出推出”。例例: 设设D= ，W= 。则则 =无扩张。无扩张。 因为可以证明关于因为可以证明关于 的算子的算子 无固定点。否则，假设无固定点。否则，假设E为为 的固定点。的固定点。如果如果 A E，则可以得到则可以得到 A E。如如果果 A E，因因为为W= ，则则 A一一定定是是由由缺缺省省规规则则D导导入入到到E的的。所所以以， A E，否则，否则，MA为假，该规则不可使用。为假，该规则不可使用。显然这是一个悖论。显然这是一个悖论。ArtificialIntelligenceResolution:122 Graduate University ,
117、Chinese academy of Sciences. 缺省逻辑缺省逻辑（6）并非所有的缺省理论都有扩张。并非所有的缺省理论都有扩张。有扩张的缺省理论也不一定是只有唯一的扩张有扩张的缺省理论也不一定是只有唯一的扩张一个理论是否有扩张一个理论是否有扩张,决定着在该理论上能否进行有效的缺省推理决定着在该理论上能否进行有效的缺省推理对于任意的闭缺省理论对于任意的闭缺省理论 和一阶闭公式集合和一阶闭公式集合S， （S）是唯一确定的。）是唯一确定的。设设 E为为 一一 阶阶 命命 题题 集集 合合 ， =为为 一一 闭闭 缺缺 省省 理理 论论 。 递递 归归 定定 义义Ei(i=0,1,2,)如下：
118、如下：E0=WEi+1=Th(Ei) w|( ：M 1,M mw) D,Ei，1,m E那么那么E是是 的一个扩张当且仅当的一个扩张当且仅当ArtificialIntelligenceResolution:123 Graduate University , Chinese academy of Sciences. 使用使用时，直接，直接删除本除本页！精品精品课件，你件，你值得得拥有有！精品精品课件，你件，你值得得拥有有！ArtificialIntelligenceResolution:124 Graduate University , Chinese academy of Sciences.
119、使用使用时，直接，直接删除本除本页！精品精品课件，你件，你值得得拥有有！精品精品课件，你件，你值得得拥有有！ArtificialIntelligenceResolution:125 Graduate University , Chinese academy of Sciences. 使用使用时，直接，直接删除本除本页！精品精品课件，你件，你值得得拥有有！精品精品课件，你件，你值得得拥有有！ArtificialIntelligenceResolution:126 Graduate University , Chinese academy of Sciences. 缺省逻辑缺省逻辑（7）关于不一致
120、的扩张有下面一些结论：关于不一致的扩张有下面一些结论：1当当且且仅仅当当W本本身身是是不不一一致致的的时时候候，闭闭缺缺省省理理论论有有一一个不一致的扩张个不一致的扩张2、若若一一个个闭闭缺缺省省理理论论有有一一个个不不一一致致的的扩扩张张，则则这这是是它它唯唯一一的的扩张；扩张；缺省理论的扩张一般是不唯一的：缺省理论的扩张一般是不唯一的：1、设设E和和F是是同同一一闭闭缺缺省省理理论论的的两两个个不不同同的的扩扩张张，则则如如果果E F，则则E=F。2、如如果果 1=， 2=为为两两个个缺缺省省理理论论，并并且且W1 W2，如如果果 2的的扩扩张张都都是是一一致致的的，那那么么 1的的扩扩张张也也是是一一致的。致的。
