《国考经典逻辑推理讲稿.ppt》由会员分享，可在线阅读，更多相关《国考经典逻辑推理讲稿.ppt（127页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、国考经典逻辑推理第一页，讲稿共一百二十七页哦2022/10/11第四章 经典逻辑推理n基本概念n命题逻辑的归结法n子句形nHerbrand定理n归结原理n归结过程的策略控制第二页，讲稿共一百二十七页哦2022/10/12基本概念n推理n什么是推理：依据一定的规则（策略）从已知的事实推出新事实（结论）的过程称为推理。第三页，讲稿共一百二十七页哦2022/10/13基本概念n推理n推理方式及其分类 p.112 演绎推理、归纳推理（完全与否）、默认推理 确定推理、不确定推理 单调推理、非单调推理 启发式推理、非启发式推理 第四页，讲稿共一百二十七页哦2022/10/14基本概念n推理n推理的控制策略
2、，即求解问题的策略。有推理方向、搜索策略、冲突消解策略、求解策略及限制策略等。n推理方向正向推理：由原始数据出发寻找可用的知识得出新事实，如此继续直至得到结论。自底向上（bottom-up），事实驱动方式。反向推理：先提出假设，由此出发，进一步寻找支持假设的证据，当所需证据与用户提供原始数据相匹配则成功。自顶向下（top-down），目标驱动方式。第五页，讲稿共一百二十七页哦2022/10/15基本概念n正向推理过程1)规则集中的规则与数据库中的事实进行匹配，得到匹配的规则集合。2)从匹配的规则集合中选择一条规则作为使用规则。3)执行使用规则的后件。将该使用规则的后件输入数据库。4)重复进行，
3、直到达到目标。第六页，讲稿共一百二十七页哦2022/10/16基本概念n正向推理算法（产生式系统）1)断言一个事实2)使事实与某个规则的前提相匹配3)完成事实和前提的合一代换4)把代换应用于规则的结论5)断言结果，并把它应用于进一步的推理6)重复1）5）第七页，讲稿共一百二十七页哦2022/10/17基本概念正向推理算法流程还有适用知识还有适用知识输入信息输入信息从从KB中选择合适知识中选择合适知识新结果存入数据库新结果存入数据库进行推理进行推理无解退出无解退出有适用知识有适用知识DB是否有解是否有解输出解输出解结果是新的结果是新的YYYYNNNN第八页，讲稿共一百二十七页哦2022/10/1
4、8基本概念n设计一正向推理系统1)能用数据库（黑板）中的事实去匹配规则的前提，若匹配不成功，能自动地进行下一条规则的匹配，在匹配时，采用什么策略等问题应考虑周到。2)若某条规则匹配成功了，系统能将此规则的结论部分自动加入数据库。3)能判断什么时候结束推理。4)能将匹配成功的规则记录下来。第九页，讲稿共一百二十七页哦2022/10/19基本概念n反向推理过程1)用规则集中的规则后件与目标事实进行匹配，得到匹配的规则集合。2)从匹配的规则集合中选择一条规则作为使用规则。3)把执行的使用规则的前件作为下一个循环的目标事实。4)重复进行，直到达到目标。第十页，讲稿共一百二十七页哦2022/10/110
5、基本概念n反向推理算法（产生式系统）1)提出获取事实（目标）的请求2)目标和任何已知的事实都不匹配3)目标和一条规则的结论匹配4)进行目标和结论的合一代换5)将代换应用于规则的前提6)这个结论成为系统的新目标7)新目标将执行动作 8)重复1）7）匹配知识库中的事实匹配规则的结论，以更进一步推理要求用户回答必要的信息失败，原目标也失败第十一页，讲稿共一百二十七页哦2022/10/111基本概念反向推理算法流程问用户问用户有此证据有此证据找一个假设找一个假设此假设为真此假设为真结结 束束在事实库在事实库有证据有证据还有假设还有假设YYYYNNNN找出结论部分找出结论部分含此假设的所含此假设的所有知
6、识有知识此假设为假此假设为假存入事实库存入事实库选一选一条知条知识让识让它的它的条件条件作为作为新假新假设设第十二页，讲稿共一百二十七页哦2022/10/112基本概念n设计一反向推理系统1)能根据用户要求或情况提出假设。2)能验证此假设是否在数据库中。3)能从知识库中将结论部分包含此假设的规则都找出来。4)能将找出来的规则的前提部分取出并作为新假设逐条验证。5)能判断假设是否是证据节点，若是，能向用户提出相应问题并记录结果。6)能将匹配成功的规则记录下来。7)能判断何时应结束推理。第十三页，讲稿共一百二十七页哦2022/10/113基本概念n推理n冲突消解策略1规则排序：规则的编排顺序就是规
7、则启用的优先级。专一性排序：若某一规则的条件部分规定的情况比另一条规则的条件部分所规定的情况更专门，则这条规则有较高的优先级。就近排序：把最近使用的规则放在最优先的位置。规模排序：按规则条件部分复杂程度排序，越复杂越优先。第十四页，讲稿共一百二十七页哦2022/10/114基本概念n推理n冲突消解策略2数据排序：把规则条件部分的所有条件项按优先级次序组织，可用知识的次序由这些知识所含条件按字典排序方法进行选择。上下文限制：按问题求解状态或新描述的上下文分块组织知识库，在某一求解状态，只能使用相对应组中的知识。数据冗余限制：若知识的操作产生上下文冗余项时，则降低该知识的优先级。第十五页，讲稿共一
8、百二十七页哦2022/10/115基本概念n模式匹配（代换与合一）n什么叫模式匹配：是指对两个知识模式（谓词公式、框架片断、语义网络片断等）的比较与耦合，即检查这两个知识模式是否完全一致或近似一致。模式匹配有确定性匹配与不确定性匹配。n什么叫合一：一个表达式（公式）的项可以是常量、变量或函数，合一就是寻找项对变量的代换而使得表达式（公式）一致的过程。合一是AI中很重要的过程。第十六页，讲稿共一百二十七页哦2022/10/116基本概念n模式匹配（代换与合一）定义4.1n代换：有序对的集合S=t1/x1,t2/x2,tn/xn 表示代换。其中ti/xi表示在公式中用ti代替xi。n例：公式 P
9、x,f(y),B s1=z/x,w/y 则 P z,f(w),B s2=A/y 则 P x,f(A),B s3=g(z)/x 则 P g(z),f(y),B n用代换s作用于公式E所得到的式子记为Es 第十七页，讲稿共一百二十七页哦2022/10/117基本概念n模式匹配（代换与合一）定义4.2n代换的复合：设有=t1/x1,t2/x2,tn/xn 和=u1/y1,u2/y2,un/yn是两个代换。则两个代换的复合也是一个代换。=t1/x1,t2/x2,tn/xn，u1/y1,u2/y2,um/ym 其中 ti xi 并且 yi x1,x2,xn n例：s1=g(x,y)/z,u/w s2=A
10、/x,B/y,C/w,D/z,w/u 则s1 s2=g(A,B)/z,A/x,B/y,w/u n性质：满足结合律，而不满足交换律（1）2=（12），而一般），而一般 12 21 第十八页，讲稿共一百二十七页哦2022/10/118基本概念n模式匹配（代换与合一）定义4.3n可合一：设有公式集合F=F1,F2,Fn,若存在一个代换使得 F1=F2=Fn，则称公式集F是可合一的。称为公式集F的一个合一。n例：F=P x,f(y),B,P x,f(B),B 则 s1=A/x,B/y 是公式集F的一个合一 s2=B/y 也是公式集F的一个合一第十九页，讲稿共一百二十七页哦2022/10/119基本概念
11、n模式匹配（代换与合一）定义4.4n最一般合一mgu(Most General Unifier)：设是公式集F的一个合一，如果对任一个合一都存在一个代换，使得=则称是一个最一般的合一。n可以证明mgu是唯一的。n求mgu算法第二十页，讲稿共一百二十七页哦2022/10/120基本概念n求mgu算法（设公式集为F）：1)令k=0,Fk=F,k=。是一个空代换。2)若Fk只含一个表达式，则算法停止，k即为所求的mgu。3)找出Fk的差异集Dk。4)若Dk中存在元素xk和tk，其中xk是变元，tk是项，且xk不在tk中出现，则置：k+1=k tk/xk ,Fk+1=Fk tk/xk ,k=k+1,然
12、后转2）5)算法终止，F的mgu不存在第二十一页，讲稿共一百二十七页哦2022/10/121基本概念n求mgu举例：F=P f(x),y,g(y),P f(x),z,g(x)k=0,F0=F,0=,D0=y,z1=0 y/z=y/zF1=F0 y/z=P f(x),y,g(y),P f(x),y,g(x)k=1,D1=y,x,2=1 y/x=y/z,y/x F2=F1 y/z,y/x=P f(y),y,g(y),P f(y),y,g(y)F2只含一个表达式，则算法停止，2即为所求的mgu。mgu=y/z,y/x第二十二页，讲稿共一百二十七页哦2022/10/122基本概念n归结原理由J.A.R
13、obinson由1965年提出。n与演绎法完全不同，新的逻辑演算算法。n一阶逻辑中，至今为止的最有效的半可判定的算法。即，一阶逻辑中任意恒真公式，使用归结原理，总可以在有限步内给以判定。n语义网络、框架表示、产生式规则等等都是以推理方法为前提的。即，有了规则已知条件，顺藤摸瓜找到结果。而归结方法是自动推理、自动推导证明用的。（“数学定理机器证明”）n本课程只讨论一阶谓词逻辑描述下的归结推理方法，不涉及高阶谓词逻辑问题。第二十三页，讲稿共一百二十七页哦2022/10/123第四章 经典逻辑推理n基本概念n命题逻辑的归结法n子句形nHerbrand定理n归结原理n归结过程的策略控制第二十四页，讲稿
14、共一百二十七页哦2022/10/124第四章 经典逻辑推理n基本概念n命题逻辑的归结法n子句形nHerbrand定理n归结原理n归结过程的策略控制第二十五页，讲稿共一百二十七页哦2022/10/125命题逻辑的归结法n归结反演推理方法基本思想例：命题：命题：A A1 1、A A2 2、A A3 3 和和 B B求证：求证：A A1 1A A2 2A A3 3成立，则成立，则B B成立，成立，即：即：A A1 1A A2 2A A3 3 B B反证法：证明反证法：证明A A1 1A A2 2A A3 3 B B 是矛盾式（永假式）是矛盾式（永假式）归结法是以子句集为背景归结法是以子句集为背景的第
15、二十六页，讲稿共一百二十七页哦2022/10/126子句的概念n子句与子句集n文字：不含任何连接词的谓词公式及其否定。n子句(定义4.5)：任何文字的析取式（谓词的和）。n空子句(定义4.6)：不含任何文字的子句。n空子句的不可满足性：由于空子句不含任何文字，它不能被任何解释满足，所以空子句是永假的，不可满足的。n子句集：由子句构成的集合。第二十七页，讲稿共一百二十七页哦2022/10/127子句的概念n建立子句集n合取范式：命题、命题和的与，如：P （PQ）（PQ）子句集S：合取范式形式下的子命题（元素）的集合例：命题公式：P（PQ）（PQ）子句集 S：S=P,PQ,PQ第二十八页，讲稿共一
16、百二十七页哦2022/10/128子句的概念n谓词公式F相对应的子句集S的求取：F SKOLEM标准形 消去全称变量 以“，”取代“”，并表示为集合形式。第二十九页，讲稿共一百二十七页哦2022/10/129命题逻辑的归结法n归结过程 n将命题写成合取范式n求出子句集n对子句集使用归结推理规则n归结式作为新子句参加归结n归结式为空子句，S是不可满足的（矛盾），原命题成立。（证明完毕）n谓词的归结：除了有量词和函数以外，其余和命题归结过程一样。第三十页，讲稿共一百二十七页哦2022/10/130第四章 经典逻辑推理n基本概念n命题逻辑的归结法n子句形nHerbrand定理n归结原理n归结过程的策
17、略控制第三十一页，讲稿共一百二十七页哦2022/10/131第四章 经典逻辑推理n基本概念n命题逻辑的归结法n子句形nHerbrand定理n归结原理n归结过程的策略控制第三十二页，讲稿共一百二十七页哦2022/10/132子句形谓词公式化为子句集步骤1n消去蕴含符号nP Q PQn例：(x)P(x)(y)P(y)P(f(x,y)(y)Q(x,y)P(y)第三十三页，讲稿共一百二十七页哦2022/10/133子句形谓词公式化为子句集步骤1n消去蕴含符号nP Q PQn例：(x)P(x)(y)P(y)P(f(x,y)(y)Q(x,y)P(y)(x)P(x)(y)P(y)P(f(x,y)(y)Q(x
18、,y)P(y)第三十四页，讲稿共一百二十七页哦2022/10/134子句形谓词公式化为子句集步骤2n减少否定符号的辖域n (P)Pn (PQ)P Q 或或 (PQ)P Q n(x)P(x)(x)P(x)或或 (x)P(x)(x)P(x)n例：(x)P(x)(y)P(y)P(f(x,y)(y)Q(x,y)P(y)第三十五页，讲稿共一百二十七页哦2022/10/135子句形谓词公式化为子句集步骤2n减少否定符号的辖域n (P)Pn (PQ)P Q 或或 (PQ)P Q n(x)P(x)(x)P(x)或或 (x)P(x)(x)P(x)n例：(x)P(x)(y)P(y)P(f(x,y)(y)Q(x,y
19、)P(y)第三十六页，讲稿共一百二十七页哦2022/10/136子句形谓词公式化为子句集步骤2n例：(x)P(x)(y)P(y)P(f(x,y)(y)Q(x,y)P(y)(x)P(x)(y)P(y)P(f(x,y)(y)Q(x,y)P(y)(x)P(x)(y)P(y)P(f(x,y)(y)Q(x,y)P(y)第三十七页，讲稿共一百二十七页哦2022/10/137子句形谓词公式化为子句集步骤3n变量标准化，即重新命名变元n保证每个量词有其唯一的约束变量。n如：(x)P(x)(x)Q(x)标准化为(x)P(x)(y)Q(y)n例：(x)P(x)(y)P(y)P(f(x,y)(y)Q(x,y)P(y
20、)第三十八页，讲稿共一百二十七页哦2022/10/138子句形谓词公式化为子句集步骤3n变量标准化，即重新命名变元n保证每个量词有其唯一的约束变量。n如：(x)P(x)(x)Q(x)标准化为(x)P(x)(y)Q(y)n例：(x)P(x)(y)P(y)P(f(x,y)(y)Q(x,y)P(y)(x)P(x)(y)P(y)P(f(x,y)(w)Q(x,w)P(w)第三十九页，讲稿共一百二十七页哦2022/10/139子句形谓词公式化为子句集步骤4n消去存在量词n如：(x)P(x,y)用 P(A,y)替换，A为某一常量。n如：(y)(x)P(x,y)引入Skolem函数g(y)，用 (y)P(g(
21、y),y)替换n例：(x)P(x)(y)P(y)P(f(x,y)(w)Q(x,w)P(w)第四十页，讲稿共一百二十七页哦2022/10/140子句形谓词公式化为子句集步骤4n消去存在量词n如：(x)P(x,y)用 P(A,y)替换，A为某一常量。n如：(y)(x)P(x,y)引入Skolem函数g(y)，用 (y)P(g(y),y)替换n例：(x)P(x)(y)P(y)P(f(x,y)(w)Q(x,w)P(w)(x)P(x)(y)P(y)P(f(x,y)Q(x,g(x)P(g(x)第四十一页，讲稿共一百二十七页哦2022/10/141子句形谓词公式化为子句集步骤4n消去存在量词 量词消去原则：
22、消去存在量词“”，略去全称量词“”。注意：左边有全称量词的存在量词，消去时该变量改写成为全称量词的函数；如没有，改写成为常量。第四十二页，讲稿共一百二十七页哦2022/10/142子句形谓词公式化为子句集步骤5n化为前束形n如把所有全称量词移到公式的左边，并使得每个量词的辖域包含这个量词后面公式的整个部分，所得公式称为前束形。n例：(x)P(x)(y)P(y)P(f(x,y)Q(x,g(x)P(g(x)第四十三页，讲稿共一百二十七页哦2022/10/143子句形谓词公式化为子句集步骤5n化为前束形n如把所有全称量词移到公式的左边，并使得每个量词的辖域包含这个量词后面公式的整个部分，所得公式称为
23、前束形。n例：(x)P(x)(y)P(y)P(f(x,y)Q(x,g(x)P(g(x)(x)(y)P(x)P(y)P(f(x,y)Q(x,g(x)P(g(x)第四十四页，讲稿共一百二十七页哦2022/10/144子句形谓词公式化为子句集步骤6n化前束形为SKOLEM标准形n前束范式：把所有的量词都提到前面去，然后消掉所有量词。定义：说公式A是一个前束范式，如果A中的一切量词都位于该公式的最左边（不含否定词），且这些量词的辖域都延伸到公式的末端。nSKOLEM标准形=（全称量词串）母式 n母式：子句的合取式第四十五页，讲稿共一百二十七页哦2022/10/145子句形谓词公式化为子句集步骤6n化前
24、束形为SKOLEM标准形n反复利用分配率，把任一个母式化为合取范式。nA(B C)(AB)(AC)n例：(x)(y)P(x)P(y)P(f(x,y)Q(x,g(x)P(g(x)第四十六页，讲稿共一百二十七页哦2022/10/146子句形谓词公式化为子句集步骤6n化前束形为SKOLEM标准形n反复利用分配率，把任一个母式化为合取范式。nA(B C)(AB)(AC)n例：(x)(y)P(x)P(y)P(f(x,y)Q(x,g(x)P(g(x)(x)(y)P(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(g(x)第四十七页，讲稿共一百二十七页哦2022/10/147子句形谓词公式化为子句集
25、步骤6n化前束形为SKOLEM标准形n反复利用分配率，把任一个母式化为合取范式。nA(B C)(AB)(AC)n例：(x)(y)P(x)P(y)P(f(x,y)Q(x,g(x)P(g(x)第四十八页，讲稿共一百二十七页哦2022/10/148子句形谓词公式化为子句集步骤6n化前束形为SKOLEM标准形例：(x)(y)P(x)P(y)P(f(x,y)Q(x,g(x)P(g(x)(x)(y)P(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(g(x)(x)(y)P(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(x)P(g(x)第四十九页，讲稿共一百二十七页哦2022/10/149
26、子句形谓词公式化为子句集步骤7n消去全称量词n例：(x)(y)P(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(x)P(g(x)P(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(x)P(g(x)第五十页，讲稿共一百二十七页哦2022/10/150子句形谓词公式化为子句集步骤8n对变元更名n使得一个变元符号不出现在一个以上的子句中。n例：P(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(x)P(g(x)P(x)P(y)P(f(x,y)P(z)Q(z,g(z)P(w)P(g(w)第五十一页，讲稿共一百二十七页哦2022/10/151子句形谓词公式化为子句集步骤9n消去
27、合取符号n用子句集代替合取式，即为所求的子句集。n例：P(x)P(y)P(f(x,y)P(z)Q(z,g(z)P(w)P(g(w)P(x)P(y)P(f(x,y)，P(z)Q(z,g(z)，P(w)P(g(w)第五十二页，讲稿共一百二十七页哦2022/10/152子句形 n定理：谓词逻辑的任意公式都可以化为与之等价的前束范式，但其前束范式不唯一。nSKOLEM标准形定义：消去量词后的谓词公式。注意：谓词公式F的SKOLEM标准形同F并不等值。第五十三页，讲稿共一百二十七页哦2022/10/153子句形nF是不可满足的 S是不可满足的nF与S不等价，但在不可满足的意义下是一致的。n定理：若F是给
28、定的公式，而S是相应的子句集，则F是不可满足的 S是不可满足的。注意：F真不一定S真，而S真必有F真。即：S F第五十四页，讲稿共一百二十七页哦2022/10/154子句形n把F的不可满足判断S的不可满足n引用Herbrand定理，研究S的不可满足性。n引用Herbrand定理，以说明归结原理的意义及一个原理形成的根基与背景 第五十五页，讲稿共一百二十七页哦2022/10/155第四章 经典逻辑推理n基本概念n命题逻辑的归结法n子句形nHerbrand定理n归结原理n归结过程的策略控制第五十六页，讲稿共一百二十七页哦2022/10/156第四章 经典逻辑推理n基本概念n命题逻辑的归结法n子句形
29、nHerbrand定理n归结原理n归结过程的策略控制第五十七页，讲稿共一百二十七页哦2022/10/157Herbrand定理n名词:公式F永真:对于F的所有解释,F都为真.公式F永假:没有一个解释使F为真.n问题：要判定一个子句集是不可满足的,就是要判定该子句集中的每一个子句都是不可满足的;要判定一个子句是不可满足的,则需要判定该子句对任何非空个体域的任意解释都是不可满足的.可见,判定子句集的不可满足性是一件非常困难的工作.第五十八页，讲稿共一百二十七页哦2022/10/158Herbrand定理n问题：一阶逻辑公式的永真性（永假性）的判定是否能在有限步内完成？第五十九页，讲稿共一百二十七页
30、哦2022/10/159Herbrand定理n1936年图灵(Turing)和邱吉(Church)互相独立地证明了：“没有一般的方法使得在有限步内判定一阶逻辑的公式是否是永真（或永假）。但是如果公式本身是永真（或永假）的，那么就能在有限步内判定它是永真（或永假）。对于非永真（或永假）的公式就不一定能在有限步内得到结论。判定的过程将可能是不停止的。”第六十页，讲稿共一百二十七页哦2022/10/160Herbrand定理nHerbrand的思想 要证明一个公式是永假的,采用反证法思想,就是寻找一个已给的公式是真的解释。然而，如果所给定的公式的确是永假的，就没有这样的解释存在，并且算法在有限步内停
31、止。因为量词是任意的，所讨论的个体变量域D是任意的，所以解释的个数是无穷的，不可数的，要找到所有解释是不可能的。第六十一页，讲稿共一百二十七页哦2022/10/161Herbrand定理nHerbrand的思想n思想：判断任何一个解释是困难的。所以简化讨论域，建立一个比较简单、特殊的域，使得只要在这个论域上，原谓词公式仍是不可满足的，即保证不可满足的性质不变。因此引入H域等概念。D域H域H域与D域关系示意图第六十二页，讲稿共一百二十七页哦2022/10/162Herbrand定理nH域nH解释n结论：Herbrand定理第六十三页，讲稿共一百二十七页哦2022/10/163Herbrand定理
32、nH域nH解释n结论：Herbrand定理第六十四页，讲稿共一百二十七页哦2022/10/164Herbrand定理（H域）nH域构造方法（定义4.7）：n设S为公式F所对应的子句集，则按下述方法构造的域H称为H域。1)令H0是S中所有个体常量的集合，若S中不含个体常量，则令H0=a，其中a为任一个体常量。2)令Hi+1=Hi S中所有形如f(x1,x2,xn)的元素，其中f(x1,x2,xn)是出现在F中任一函数符号，i=0,1,2,3,。例题请参考教科书P128第六十五页，讲稿共一百二十七页哦2022/10/165Herbrand定理（H域）n例题1:S=P(a),P(x)P(f(x),求
33、H域。H0=a H1=a,f(a)H2=a,f(a),f(f(a)H=H0H1H2.=a,f(a),f(f(a),n例题2:S=P(z),P(x)Q(y),求H域。H0=a H1=a H2=aH=H0H1H2.=a 第六十六页，讲稿共一百二十七页哦2022/10/166Herbrand定理（H域）n例题3:S=P(x),Q(y,f(z,b),R(a),求H域。H0=a,bH1=a,b,f(a,b),f(b,b)H2=a,b,f(a,b),f(b,b),f(f(a,b),b),f(f(b,b),b),H=H0H1H2.=a,b,f(a,b),f(b,b),第六十七页，讲稿共一百二十七页哦2022
34、/10/167Herbrand定理（H域）n几个基本概念n基子句：用H域中的元素代换子句中的变元所得到的子句，即不含变量的子句。n基原子：基子句中的谓词，即没有变量出现的原子。n原子集A：子句集中所有基原子构成的集合。如A=所有形如 P(t1,t2,tn)的元素（其中P(t1,t2,tn)是出现于S中的任一谓词符号，而t1,t2,tn 是S的H域的任意元素）即把H中的东西填到S的谓词里去。S中的谓词是有限的，H是可数的，因此，A也是可数的。第六十八页，讲稿共一百二十七页哦2022/10/168Herbrand定理（H域）n原子集举例:nS=P(a),P(x)P(f(x),H=a,f(a),f(
35、f(a),A=P(a),P(f(a),P(f(f(a),nS=P(z),P(x)Q(y),H=a A=P(a),Q(a)nS=P(x),Q(y,f(z,b),R(a),H=a,b,f(a,b),f(a,a),f(b,a),f(b,b),A=P(a),P(b),Q(a,a),Q(a,b),R(a),R(b),第六十九页，讲稿共一百二十七页哦2022/10/169Herbrand定理（H域）n原子集n一旦原子集内真值确定好（规定好），则S在H上的真值可确定。S中的谓词是有限的，可数的，H域中的元素是可数的，因此，原子集A中的元素也是可数的。n由此可见，在无限不可数的个体域D上的问题转化成为可数的问
36、题。n 把谓词公式的不可满足性讨论从D转换到H域，其复杂程度得到相应减少。不可解问题变为可解问题。第七十页，讲稿共一百二十七页哦2022/10/170Herbrand定理nH域nH解释n结论：Herbrand定理第七十一页，讲稿共一百二十七页哦2022/10/171Herbrand定理nH域nH解释n结论：Herbrand定理第七十二页，讲稿共一百二十七页哦2022/10/172Herbrand定理（H解释）nH解释I（定义4.8）：取一个值得到一个结论n解释I：谓词公式F在论域D上任何一组真值的指定称为一个解释。公式F的一个解释就是公式F在其论域上的一个实例化。nH解释：子句集S在其H域上的
37、解释称为H解释。n子句集S在H域上的一个解释I满足下列条件：1)I映射S中所有常量符号到它们本身。(即原子集)2)令f是n元函数，I是f下的一个指派，即H中的元素到f的一个映射（函数值）。简单地说(P129)，A中的各元素真假组合都是H的解释。（或真或假只取一个）第七十三页，讲稿共一百二十七页哦2022/10/173Herbrand定理（H解释）例：子句集S=P(x)Q(x),R(f(y)有 H域 H=a,f(a),f(f(a),原子集A=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),凡是对A中各元素真假值的一个具体设定都是S的一个H解释。如 I1*=P(a),Q(a
38、),R(a),Q(f(a),R(f(a),I2*=P(a),Q(a),R(a),Q(f(a),R(f(a),I3*=P(a),Q(a),R(a),Q(f(a),R(f(a),I1*I2*I3*中出现的P(a)指P(a)取值为T，出现的 P(a)指P(a)取值为F。第七十四页，讲稿共一百二十七页哦2022/10/174Herbrand定理（H解释）I1*I2*I3*中出现的P(a)指P(a)取值为T，出现的 P(a)指P(a)取值为F。显然在H域上，这样定义I*下，S的真假值就确定了。如n问题：对于所有的解释，全是假才可判定。因为所有解释代表了所有的情况，如果可以被穷举，问题便可解决。一般来说，
39、一个子句集的基原子有无限多个，它在H域上的解释也有无限多个。S的不可满足问题 H上的不可满足问题，有Herbrand定理支持。第七十五页，讲稿共一百二十七页哦2022/10/175Herbrand定理（H解释）n如下三个定理保证了归结法的正确性：n定理1（定理4.2）：设I是S的论域D上的解释，存在对应于I的H解释I*，使得若有S|I=T，必有 S|I*=T。n定理2（定理4.2）：子句集S是不可满足的，当且仅当所有的S的H解释下为假。n定理3（定理4.3）：子句集S是不可满足的，当且仅当对每一个解释I下，至少有S的某个子句的某个基例为假。第七十六页，讲稿共一百二十七页哦2022/10/176
40、Herbrand定理（H解释）n基例S中某子句中所有变元符号均以S的H域中的元素代入时，所得的基子句C称为C的一个基例。n若一个子句为假，则此解释为假。n一般来说，D是无穷不可列的，因此，子句集S也是无穷不可列的。但S确定后H是无穷可列的。不过在H上证明S的不可满足性仍然是不可能的。n计算机实现是困难的，提出归结原理第七十七页，讲稿共一百二十七页哦2022/10/177Herbrand定理nH域nH解释n结论：Herbrand定理第七十八页，讲稿共一百二十七页哦2022/10/178Herbrand定理nH域nH解释n结论：Herbrand定理第七十九页，讲稿共一百二十七页哦2022/10/1
41、79Herbrand定理（结论）Herbrand定理：子句集S是不可满足的，当且仅当存在不可满足的S的有限基例集。第八十页，讲稿共一百二十七页哦2022/10/180Herbrand定理（结论）n定理的意义nHerbrand定理已将证明问题转化成了命题逻辑问题。n由此定理保证，可以放心的用机器来实现自动推理了。（归结原理）n注意nHerbrand定理给出了一阶逻辑的半可判定算法，即仅当被证明定理是成立时，使用该算法可以在有限步得证。而当被证定理并不成立时，使用该算法得不出任何结论。但是 第八十一页，讲稿共一百二十七页哦2022/10/181Herbrand定理（结论）n仍存在的问题：基例集序列
42、元素的数目随子句集的元素数目成指数增加。n因此，Herbrand定理是30年代提出的，始终没有显著的成绩。直至1965年Robinson提出了归结原理，才使得Herbrand定理的光彩得以发挥。第八十二页，讲稿共一百二十七页哦2022/10/182第四章 经典逻辑推理n概述n命题逻辑的归结法n子句形nHerbrand定理n归结原理n归结过程的策略控制第八十三页，讲稿共一百二十七页哦2022/10/183归结原理n基本思想 通过归结方法不断扩充待判定的子句集，并设法使其包含指示矛盾的空子句。n空子句是不可满足（即永假）的子句（P.126），既然子句集中子句间隐含着合取关系，空子句的出现实际上判定
43、了子句集的不可满足。n定义4.9：若P是原子谓词公式，则称P与 P为互补文字。第八十四页，讲稿共一百二十七页哦2022/10/184命题逻辑的归结法n归结（定义4.10）设有子句C1,C2，如果C1中的文字L1与C2中的文字L2互补，则消除互补对，余下部分析取求得新子句 得到归结式C12。例：C1 C2 C12 P P Q Q 假言推理 P Q P Q Q Q=Q 合并 P Q P Q Q Q 重言式 P Q P Q P P P P 或 NIL 空子句 P Q Q R P R 三段论第八十五页，讲稿共一百二十七页哦2022/10/185命题逻辑的归结法n归结式性质n定理4.4：两个子句C1和C
44、2的归结式C12是C1和C2的逻辑推论，即C1C2 C12（在任一个使子句C1和C2为真的解释I下，必有归结式C12为真）推论1：子句集S中子句C1和C2的归结式为C12，若用C12 代替C1和C2后得到新子句集S1，则S1不可满足性 S的不可满足性 推论2：子句集S中子句C1和C2的归结式为C12，若把C12 加入S中得到新子句集S2，则S2不可满足性 S的不可满足性 第八十六页，讲稿共一百二十七页哦2022/10/186谓词逻辑的归结法n归结（含有变量子句的归结，定义4.11）设有两个没有相同变元的子句C1,C2，L1是C1中的文字与L2是C2中的文字，若是L1和L2的mgu，则称C12=
45、(C1 -L1 )(C2 -L2 )为子句C1,C2的二元归结式。第八十七页，讲稿共一百二十七页哦2022/10/187谓词逻辑的归结法例：Px,f(A)Px,f(y)Q(y)Pz,f(A)Q(z)取L1为Px,f(A)，L2为 Pz,f(A)则=x/z 得C12=Px,f(y)Q(y)Q(x)例：Px,f(A)Px,f(y)Q(y)Pz,f(A)Q(z)取L1为Q(y)，L2为 Q(z)则=y/z 得C12=Px,f(A)Px,f(y)Py,f(A)可进一步归结得到 Px,f(x)第八十八页，讲稿共一百二十七页哦2022/10/188谓词逻辑的归结法例：Px,f(A)Px,f(y)Q(y)P
46、z,f(A)Q(x)修改C2变元名 Pz,f(A)Q(x1)取L1为Px,f(A)，L2为 Pz,f(A)则=x/z 得C12=Px,f(y)Q(y)Q(x)则=x/z 得C12=Px,f(y)Q(y)Q(x1)第八十九页，讲稿共一百二十七页哦2022/10/189归结反演n归结原理正确性的根本在于，找到矛盾可以肯定不真。n方法：n和命题逻辑一样。n但由于有函数，所以要考虑合一和置换。第九十页，讲稿共一百二十七页哦2022/10/190归结反演n置换和合一的注意事项：1.谓词的一致性，P()与Q()，不可以2.常量的一致性，P(a,)与P(b,.)，不可以 变量，P(a,.)与P(x,)，可以
47、3.变量与函数，P(a,x,.)与P(x,f(x),)，不可以；但P(a,z,)与P(x,f(y),)，可以1.不能同时消去两个互补对，PQ与 P Q的空，不可以n先进行内部简化（置换、合并）第九十一页，讲稿共一百二十七页哦2022/10/191归结反演在定理证明中的应用在定理证明中的应用n归结反演的基本思想 目标公式被否定并化为子句集，添加到命题公式集中，用归结反演应用于联合集，并力图推导出一个空子句（或 NIL）表示产生一个矛盾，定理得证。第九十二页，讲稿共一百二十七页哦2022/10/192归结反演在定理证明中的应用在定理证明中的应用n归结反演的过程（证明F Q）(P.133)n写出谓词
48、关系公式F（前提）和Q（目标、结论）n否定目标Q加入公式集F,写出谓词表达式 F,Qn求SKOLEM标准形 n化为子句集S n对S中可归结的子句做归结 n归结式仍放入S中，反复归结过程 n得到空子句(NIL)，得证第九十三页，讲稿共一百二十七页哦2022/10/193归结反演在定理证明中的应用在定理证明中的应用n证明：每个储蓄钱的人都获得利息，若没有利息就没有人去储蓄钱。令：S(x,y)表示x储蓄y M(x)表示x是钱 I(x)表示x是利息 E(x,y)表示x获得y则前提为(x)(y)(S(x,y)M(y)(y)(I(y)E(x,y)结论为 (x)I(x)(x)(y)(S(x,y)M(y)第九
49、十四页，讲稿共一百二十七页哦2022/10/194归结反演在定理证明中的应用在定理证明中的应用F:(x)(y)(A(x,y)B(y)(y)(C(y)D(x,y)G:(x)C(x)(x)(y)(A(x,y)B(y)F化为子句得 A(x,y)B(y)C(f(x).(1)A(x,y)B(y)D(x,f(x).(2)G化为子句得 C(z).(3)A(a,b).(4)B(b).(5)第九十五页，讲稿共一百二十七页哦2022/10/195归结反演在定理证明中的应用在定理证明中的应用 A(x,y)B(y)D(x,f(x)A(x,y)B(y)C(f(x)C(z)A(a,b)B(b)(1)(2)(3)(4)(5
50、)NIL(8)B(b)C(f(a)(6)a/x,b/y B(b)(7)f(a)/z第九十六页，讲稿共一百二十七页哦2022/10/196归结反演在定理证明中的应用在定理证明中的应用归结反演基本算法：给定公式F对应的子句集S，求证目标公式G成立。CLAUSESSG Until NIL 是CLAUSES的成员，do：begin 在子句集CLAUSES中选择二个不同的可归结的子句 Ci,Cj 计算Ci,Cj的归结式Cij CLAUSES将Cij加入到CLAUSES中 end说明：可归结子句的选择次序可以是任意的。第九十七页，讲稿共一百二十七页哦2022/10/197归结反演在定理证明中的应用在定理证