人工智能原理 ch4.1_经典逻辑推理.ppt

2020 3 24 1 人工智能原理 第四讲经典逻辑推理 主讲 王祖喜zuxiw 华中科技大学图像所 2020 3 24 2 经典逻辑推理经典逻辑推理是根据经典逻辑的逻辑规则进行的一种推理 又称为机械 自动定理证明 mechanical automatictheoremproving 主要推理方法有自然演绎推理 归结演绎推理及与或形演绎推理等 由于这种推理是基于经典逻辑的 其真值只有真和假两种 因此它是一种精确推理 学习目的 学习运用知识进行推理 求解问题 2020 3 24 3 主要讲述内容 1 简述与推理相关的知识 如推理方式及分类 推理控制策略 模式匹配 冲突消解策略 搜索策略等 2 经典逻辑推理 自然演绎推理 归结演绎推理和与 或形演绎推理 2020 3 24 4 什么是推理推理从已知事实出发 运用已掌握的知识 找出其中蕴含的事实 或归结出新的事实 这一过程称为推理 推理机在人工智能中 推理是由程序实现的 称为推理机 推理包括两种判断 一种是已知的判断 它包括已掌握的与求解问题有关的知识以及关于问题的已知事实 另一种是由已知判断推出的新判断 即推理的结论 推理的基本任务 是从一种判断推出另一种判断 1推理的基本概念 2020 3 24 5 一般而言 推理有一下五种划分方式 演绎推理 归结推理 默认推理 从新判断推出的途径来划分 演绎推理 从全称判断推导出特称判断或单称判断的过程 即由一般性知识推出适合于某一具体情况的结论 这是一种从一般到个别的推理 演绎推理有多种形式 经常用的是三段论式 它包括 1 大前提 这是已知的一般性知识或假设 2 小前提 这是关于所研究的具体情况或个别事实的判断 推理的方式及其分类 2020 3 24 6 3 结论 这是由大前提推出的适合于小前提所示情况的新判断 例如 1 足球运动员的身体都是强壮的 2 高波是一名足球运动员 3 所以 高波的身体是强壮的 这就是一个三段论推理 其中 1 是大前提 2 是小前提 3 是经演绎推出的结论 结论 高波的身体是强壮的 事实上是蕴含于 足球运动员的身体都是强壮的 这一大前提中的 它没有超出 2020 3 24 7 大前提所断定的范围 这是演绎推理的一个典型特征 即在任何情况下 由演绎推理导出的结论都是蕴含在大前提的一般性知识中的 因此 只要大前提和小前提是正确的 则由它们推导出来的结论也必然是正确的 演绎推理是人工智能中的一种重要推理方式 在直到目前研制成功的各类智能系统中 大多是用演绎推理实现的 2020 3 24 8 归结推理 归结推理是从足够多的事例中归结出一般性结论的推理过程 是一种从个别到一般的推理 归结推理又分为完全归结和不完全归结两种 完全归结 指在进行归结时考察了相应事物的全部对象 并根据这些对象是否都有某种属性 从而推出这种事物是否具有这个属性 例如 某厂进行产品质量检查 如果对每一件产品都进行了严格检查 并且是合格的 则推导出结论该厂的产品是合格的 不完全归结 指只考察了相应事物的部分对象 就得出了结论 2020 3 24 9 默认推理 又称缺省推理 它是在知识不完全的情况下假设某些条件已经具备所进行的推理 在默认推理过程中 如果到某一时刻发现原先所作的默认不正确 则就要撤销所作默认 以及由此默认推出的所有结论重新按新情况进行推理 确定性推理 不确定性推理 按推理时所用知识的确定性来划分 确定性推理 指推理时所用的知识都是精确的 推出的结论也是确定的 其真值或为 真 或为 假 没有第三种情况出现 下面将要讨论的经典逻辑推理就属于这一类 2020 3 24 10 不确定性推理 指推理时所用的知识不都是精确的 推出的结论也不完全是肯定的 其真值位于 真 和 假 之间 命题的外延模糊不清 这里我们要特别强调不确定性推理 自亚里士多德建立第一个演绎公理系统以来 经典逻辑与精确数学的建立与发展为人类科学技术的发展起了巨大的作用 然而 现实世界中的事物和现象大都是不严格 不精确的 许多概念是模糊的 很难用精确的数学模型来表示和处理 因此 近几年来 各种非经典逻辑迅速崛起 人工智能亦把不精确知识的表示与处理作为重要的研究课题 另外 从人类思维活动的特征来看 人们经常是在知识不完全 不精确的情况下进行多方位的思考及推理的 因此 要使计算机模拟人类的思维活动 就必须使其具有不确定性推理的能力 2020 3 24 11 单调推理 非单调推理 按推理过程中推出的结论是否单调的增加来划分 单调推理 指在推理过程中随着推理的向前推进及新知识的加入 推出的结论呈单调增加的趋势 并且越来越接近最终目标 在推理过程中不会出现反复的情况 即不会由于新知识的加入而否定前面推出的结论 使推理又退回到前面的一步 非单调推理 指在推理过程中由于新知识的加入 不仅没有加强已推出的结论 反而要否定它 使得推理退回到前面的某一步 重新开始 2020 3 24 12 启发式推理 非启发式推理 按推理中是否运用与问题有关的启发性知识分 启发式推理 推理中运用与问题有关的启发性知识 即解决问题的策略 技巧 窍门 对解的特性及规律的估计等实践经验和知识以加快推理过程 提高搜索效率 这种推理称为启发式推理 非启发式推理 比如穷举式推理等 2020 3 24 13 基于知识的推理 统计推理 直觉推理 从方法论的角度划分 基于知识的推理 根据已掌握的事实 通过运用知识进行的推理 统计推理 根据对某事物的数据统计进行的推理 相当于归纳推理 直觉推理 又称常识性推理 是根据常识进行的推理 2020 3 24 14 推理过程是一个思维过程 即求解问题的过程 求解问题的质量和效率不仅依赖于所采用的求解方法 而且还依赖于求解问题的策略 即推理的控制策略 推理的控制策略主要包括 推理方向 搜索策略 冲突消解策略 求解策略及限制策略等 推理的控制策略 2020 3 24 15 推理方向用于确定推理的驱动方式 分为正向推理 逆向推理 混合推理和双向推理四种 无论按哪种方向进行推理 一般都要求系统具有一个存放知识的知识库 一个存放初始已知事实及问题状态的数据库和一个用于推理的与推理机 推理方向 2020 3 24 16 正向推理 正向推理是以已知事实作为出发点的一种推理 又称数据驱动推理 前向链推理及前件推理等 正向推理的基本思想 从用户提供的初始已知事实出发 在知识库KB中找出当前可适用的知识 构成可适用知识集KS 然后按某种冲突消解策略从KS中选出一条知识进行推理 并将推出的新事实加入到数据库中作为下一步推理的已知事实 在此之后再在知识库中选取可适用的知识进行推理 如此重复 直到求得了所要求的解 或者知识库中再无可适用的知识为止 2020 3 24 17 正向推理过程算法描述 2020 3 24 18 与正向推理相关的问题 匹配方法 在以上推理过程中 需要从知识库KB中选出可适用的知识 这就要用知识库中的知识与数据库中的已知事实进行匹配 为此需确定匹配方法 搜索策略 为了进行匹配 就要查找知识 这就牵涉到按什么路线进行查找的问题 既按什么搜索策略搜索知识库 冲突消解策略 如果适用的知识只有一条 这比较简单 系统立即就可用它进行推理 并将推出的新事实送入数据库DB中 但是 如果当前适用的知识有多条 应该先用那一条 这是推理中的一个重要问题 称为冲突消解策略 总之 为了实现正向推理 有许多具体问题需要解决 2020 3 24 19 例 设在综合数据库中存放有下列已知事实 该动物身上有暗斑点 长脖子 长腿 有奶 有蹄且假设综合数据库中的已知事实与规则库中的知识是从第一条开始 逐条进行匹配的 则推理机构的工作过程如下 从规则库中取出第一条规则r1 检查前提条件与综合数据库中的已知事实不匹配 取第二条规则r2 r2的前提 该动物有奶 与综合数据库中事实匹配 则rr被执行 其结论被加入综合数据库中 此时综合数据库中的事实为 该动物身上有暗斑点 长脖子 长腿 有奶 有蹄 是哺乳动物 正向推理求解过程 2020 3 24 20 接着取r3r4r5r6都不匹配 取到r7时 匹配成功 则将r7的结论加入综合数据库 该动物身上有暗斑点 长脖子 长腿 有奶 有蹄 是哺乳动物 是有蹄动物 接着取规则 取到r11时 匹配成功 发现其前提条件与综合数据库完全匹配 则确定该动物是 长颈鹿至此 问题的求解结束了 2020 3 24 21 逆向推理是以某个假设目标作为出发点的一种推理 又称为目标驱动推理 逆向链推理及后件推理等 逆向推理的基本思想 首先选定一个假设目标 然后寻找支持该假设的证据 若所需的证据都能找到 则说明原假设成立 若无论如何都找不到所需证据 说明原假设不成立 此时需要另作新的假设 推理过程算法描述 图示 逆向推理 2020 3 24 22 逆向推理过程算法描述 2020 3 24 23 假设某用户希望动物识别系统验证一下某动物是否是虎 并设当前数据库为空 其逆向推理过程为 以虎作为假设目标 检察数据库中有无虎这个事实 因为数据库初始为空 显然不会有虎这个事实 判断该目标是否是证据 判断一个目标是否是证据 只要检查它是否为某条知识的结论就可得知 如果它不包含在任何一条知识的结论部分中 那么它就是证据 这里虎显然不是证据 因为它是规则r10的结论 逆向推理求解过程 2020 3 24 24 在知识库中找出所有能导出该目标的知识 该问题比较简单 只有一条知识可导出结论虎 即r10 r10 If该动物是哺乳动物and是食肉动物and是黄褐色and身上有黑色条纹then该动物是虎 将r10的运用条件分别作为新的假设进行验证 该知识有一个运用条件是 是黄褐色 当把它作为新假设进行推理时 首先要检查数据库中有无该事实 这里显然没有 2020 3 24 25 接着判断它是否是证据 因在r1 r15中没有一条知识的结论部分包含它 所以它是证据 此时询问用户 你看到的动物是黄褐色吗 若用户答是 则该运用条件就得到了验证 并将它存入数据库中 若用户回答不是 则就否定了原先关于虎的假设 需要作另外的假设 从头开始进行逆向推理 这里 我们假设用户的回答为是 以便将推理进行下去 对于知识的运用条件 身上有黑条纹 与上面处理类似 因为它也是一个证据 我们同样假定用户的回答为是 这样数据库中就又增加了一个事实 2020 3 24 26 现在数据库中有两个事实 是黄褐色 身上有黑条纹 对于知识的运用条件 是哺乳动物 因它没有在数据库中出现 同时又不是证据 它是r1与r2的结论 所以要在知识库中找出能导出它的所有知识 即r1与r2 r1 If该动物有毛发then该动物是哺乳动物r2 If该动物有奶then该动物是哺乳动物 2020 3 24 27 此时 因同时有两条知识可供使用 因而存在先使用哪一个的问题 这有多种处理方法 将在以后讨论 这里我们采用最简单的一种 即哪一个排在前面就先使用哪一个 所以用r1 由于r1的运用条件是有毛发 因此又要把有毛发作为新假设进行验证 显然它是一个证据 经询问用户 假定回答为是 这样 是哺乳动物就被肯定 对于运用条件 是食肉动物 可作类似处理 只是为证实它 要用到r5或r6 2020 3 24 28 r5 If该动物吃肉then该动物是食肉动物r6 If该动物有犬齿and有爪and眼盯前方then该动物是食肉动物使用r5时 若用户对询问 该动物吃肉吗 给出肯定的回答 至此r10的四个运用条件都被证实 从而肯定原假设 该动物是虎 的正确性 2020 3 24 29 逆向推理的主要优点 不必使用与目标无关的知识 目的性强 同时还有利于向用户提供解释 逆向推理的主要缺点 初始目标的选择有盲目性 若不符合实际 就要多次提出假设 影响到系统效率 2020 3 24 30 正 逆向推理存在的缺陷正向推理 具有盲目 效率低等缺点 逆向推理 若提出的假设目标不符合事实 也会降低系统效率 为解决这些问题 可把正向推理与逆向推理结合起来 取长补短 象这样既有正向又有逆向的推理称为混合推理 混合推理 2020 3 24 31 混合推理的两种情况 先正向再逆向 先进行正向推理 帮助选择某个目标 即从已知事实演绎出部分结果 然后再用逆向推理证实该目标或提高其可信度 2020 3 24 32 先逆向再正向 先假设一个目标进行逆向推理 然后再利用逆向推理中得到的信息进行正向推理 以推出更多的结论 2020 3 24 33 双向推理是指正向推理与逆向推理同时进行 且在推理过程中的某一步骤上 碰头 的一种推理方式 基本思想 一方面根据已知事实进行正向推理 但并不推到最终目标 另一方面从某假设目标出发进行逆向推理 但并不推至原始事实 而是让它们在中途相遇 即由正向推理所得的中间结论恰好是逆向推理此时所需要的证据 这时推理就可结束 逆向推理时所做的假设就是推理的最终结论 双向推理 2020 3 24 34 求解策略所谓推理的求解策略是指 推理是只求一个解 还是求所有解以及最优解等 限制策略为了防止无穷的推理过程 以及由于推理过程太长增加时间及空间的复杂性 可在控制策略中指定推理的限制条件 以对推理的深度 宽度 时间 空间等进行限制 求解策略和限制策略 2020 3 24 35 A概念在推理过程中 系统要不断地用当前已知的事实与知识库中的知识进行匹配 此时可能发生如下三种情况 已知事实不能与知识库中的任何知识匹配成功 已知事实恰好只与知识库中的一个知识匹配成功 已知事实可以与知识库中的多个知识匹配成功 或者有多个 组 已知事实都可与知识库中的一个知识匹配成功 或者有多个 组 已知事实可与知识库中的多个知识匹配成功 第三种情况为发生了冲突 此时需要按一定的策略解决冲突 以便从中挑选一个知识用于当前的推理 称这一解决冲突的过称为冲突消解 解决冲突时所用的方法称为冲突消解策略 冲突消解策略 2020 3 24 36 B以产生式系统为例进行较详细说明 产生式系统冲突在产生式系统中 若出现下列情况就认为发生了冲突 对正向推理而言 如果有多条产生式规则的前件都和已知事实匹配成功 或者有多组不同的已知事实都与同一条产生式规则的前件匹配成功 或者以上两种情况同时出现 对逆向推理而言 如果有多条产生式规则的后件都和同一个假设匹配成功 或者有多条产生式规则的后件可与多个假设匹配成功 2020 3 24 37 冲突消解冲突消解的任务是解决冲突 对正向推理来说 它将决定选择哪一组已知事实来激活哪一条产生式规则 使它用于当前的推理 产生其后件指出的结论或执行相应的操作 对逆向推理来说 它将决定用哪一个假设与哪一个产生式规则的后件进行匹配 从而推出相应的前件 作为新的假设 2020 3 24 38 冲突消解策略目前已有多种消解冲突的策略 其基本思想都是对知识进行排序 常用的有以下几种 按针对性排序 本策略是优先选用针对性较强的产生式规则 设有如下两条产生式规则 r1 IFA1ANDA2AND ANDAnTHENH1r2 IFB1ANDB2AND ANDBmTHENH2如果存在最一般合一 使得r1中每一个Ai都可变成相应的Bi 即r2中包含r1的全部条件A1 A2 An外 还包含其他条件 则称r2比r1有更大的针对性 r1比r2有更大的通用性 2020 3 24 39 按已知事实的新鲜性排序 把数据库中后生成的事实称为新鲜的事实 在产生式的推理过程中 每应用一条产生式规则就会得到一个或多个结论或者执行某个操作 数据库就会增加新的事实 另外 在推理时还会向用户询问有关的信息 也使数据库的内容发生变化 我们把数据库中后生成的事实称为新鲜的事实 即后生成的事实比先生成的事实具有较大的新鲜性 若一条规则被应用后生成了多个结论 则即可以认为这些结论有相同的新鲜性 也可认为排在前面的结论有较大的新鲜性 根据情况而定 2020 3 24 40 按匹配度排序 匹配度大的知识优先选用 在不确定性匹配中 为了确定两个知识模式是否匹配 需要计算这两个模式的相似程度 当其达到某个预先规定的值时 则认为它们是可匹配的 相似度又称为匹配度 若产生式规则r1 r2都可匹配成功 则可根据它们的匹配度决定哪个规则被优先选用 2020 3 24 41 根据领域问题的特点排序某些领域问题 预先可知道它的某些特点 此时可根据这些特点把知识排成固定的顺序 例如 1 当领域问题有固定的解题次序时 可按该次序排列相应的知识 排在前面的知识优先被应用 2 当已知某些产生式规则被应用后会明显的有利于问题的求解时 就使这些产生式规则优先被应用 2020 3 24 42 按上下文限制排序把产生式规则按它们所描述的上下文分成若干组 在不同的条件下 只能从相应的组中选取有关的产生式规则 这样 不仅可以减少冲突的发生 而且由于搜索范围小 也提高了推理效率 按冗余限制排序如果一条产生式规则被应用后将产生冗余知识 则降低了它被应用的优先级 产生的冗余知识越多 优先级越低 按条件个数排序如果有多条产生式规则生成的结论相同 则要求条件少的产生式规则被优先应用 因为要求条件少的规则匹配时花费的时间较少 2020 3 24 43 1 基本概念所谓模式匹配是指对两个知识模式 如两个谓词公式 两个框架片断或两个语义网络片断等 的比较与耦合 即检查这两个知识模式是否完全一致或近似一致 如果两者完全一致 或虽不完全一致但其相似程度落在指定的限度内 就称它们是可匹配的 否则为不可匹配 模式匹配是推理中必须进行的一项重要工作 因为只有经过模式匹配才能从知识库中选出当前适用的知识 才能进行推理 模式匹配 2020 3 24 44 2 分类若按匹配时两个知识模式的相似程度分 可分为确定性匹配和不确定性匹配两种 确定性匹配 指两个知识模式完全一致 或经过变量代换后变的完全一致 例如 设有两个知识模式 P1 father 李四 李小四 andman 李小四 P2 father x y andman y 若用 李四 代换变量x 用 李小四 代换y 则P1 P2就变得完全一致 若用这两个知识模式进行匹配 则称它们是确定性匹配 确定性匹配又称完全匹配或精确匹配 2020 3 24 45 不确定性匹配 指两个知识模式不完全一致 但从总体上看 其相似程度又落在指定的限度内 2020 3 24 46 3 变量代换无论是确定性匹配或不确定性匹配 在进行匹配时一般都需要进行变量的代换 定义1 代换是形如 t1 x1 t2 x2 tn xn 的有限集合 其中 t1 t2 tn是项 x1 x2 xn是互不相同的变元 ti xi表示用ti代xi换 不允许ti与xi相同 也不允许变元xi循环地出现在另一个tj中 例如 a x f b y w z 是一个代换 g y x f x y 不是一个代换 2020 3 24 47 因为代换的目的是使某些变元被另外的变元 常量或函数取代 使之不再在公式中出现 而 g y x f x y 在x与y之间出现了循环代换的情况 它既没有消去x 也没有消去y 如果将它改为 g a x f x y 则是一个代换它将把公式中的x用g a 代换 y用f g a 代换 从而消去了变元x和y 2020 3 24 48 定义2 设 t1 x1 t2 x2 tn xn u1 y1 u2 y2 um ym 是两个代换 则此两个代换的复合也是一个代换 是从 t1 x1 t2 x2 tn xn u1 y1 u2 y2 um ym 中删去如下两种元素 ti xi当ti xiui yi当yi x1 x2 xn 后剩下的元素所构成的集合 记为 o 例如 设有代换 f y x z y a x b y y z 则 o f b x y z 2020 3 24 49 定义3 设有公式集F F1 F2 Fn 若存在一个代换 使得F1 F2 Fn 则称 为公式集F的一个合一 且称F1 F2 Fn是可合一的 例如 假设有公式集F P x y f y P a g x z 则下式是它的一个合一 a x g a y f g a z 一个公式集的合一一般来说是不唯一的 2020 3 24 50 定义4 设 是公式集F的一个合一 如果对任一个合一 都存在一个代换 使得 o 则称 是一个最一般的合一 最一般的合一是唯一的 若用最一般合一去代换那些可合一的谓词公式 可使它们变成完全一致的谓词公式 由此可知 为了使两个知识模式匹配 可用其最一般的合一对他们进行代换 2020 3 24 51 差异集的概念 设有如下两个谓词公式 F1 P x y z F2 P x f a h b 分别从F1与F2的第一个符号开始 逐个向右比较 此时发现F1中的y与F2中的f a 不同 它们构成了一个差异集 D1 y f a 当继续向右比较时 又发现F1中的z与F2中的h b 不同 则又得到一个差异集 D2 z h b 2020 3 24 52 下面给出求取最一般合一算法的具体步骤 1 令k 0 Fk F k 这里 F是欲求其最一般合一的公式集 是空代换 它代表不作代换 2 若Fk只含一个表达式 则算法停止 k就是最一般合一 3 找出Fk的差异集Dk 4 若Dk中存在元素xk和tk 其中xk是变元 tk是项 且xk不在tk中出现 则置 k 1 ko tk xk 求取最一般合一的算法 2020 3 24 53 Fk 1 Fk tk xk k k 1然后转 2 5 算法中止 F的最一般合一不存在 2020 3 24 54 例如 设F P a x f g y P z f z f u 求其最一般合一 1 令 0 F0 F 因F0中含有两个表达式 所以 0不是最一般合一 2 差异集D0 a z 3 1 0o a z a z F1 P a x f g y P a f a f u 4 D1 x f a 求取实例 2020 3 24 55 5 2 1o f a x a z f a x F2 F1 f a x P a f a f g y P a f a f u 6 D2 g y u 7 3 2o g y u a z f a x g y u 8 F3 F2 g y u P a f a f g y 因为F3只含一个表达式 所以 3就是最一般合一 即 a z f a x g y u 2020 3 24 56 经典逻辑推理是根据经典逻辑 命题逻辑和一阶谓词逻辑 的逻辑规则进行的一种推理 又称机械 自动定理证明 主要推理方法有自然演绎推理 归结演绎推理和与 或形演绎推理等 这种推理是基于经典逻辑的 其真值只有 真 与 假 两种 因此它是一种精确推理 或称为确定性推理 2经典逻辑推理 2020 3 24 57 数学基础 谓词演算 1 谓词公式P x1 x2 xn 其中 P是谓词名 x1 x2 xn是个体 在谓词中 个体可以是常量 变元 也可以是函数 个体变元的取值范围称为个体域 2020 3 24 58 2 谓词公式的解释 定义1 设D为谓词公式P的个体域 若对P中的个体常量 函数和谓词按如下规定赋值 为每个个体常量指派D中的一个元素 为每个n元函数指派一个从Dn到D的映射 其中Dn x1 x2 xn x1 x2 xn D 为每个n元谓词指派一个从Dn到 F T 的映射 则称这些指派为公式P在D上的一个解释 2020 3 24 59 例1 设个体域D 1 2 求公式A x y P x y 在D上的解释 并指出在每一种解释下公式A的真值 在公式中没有个体常量和函数 所以直接给谓词指派真值 设为 P 1 1 T P 1 2 F P 2 1 T P 2 2 F这就是谓词公式A在D上的一个解释 公式A的真值为 T 即对所有的x 1 2 都存在一个y 1 使P x y T 2020 3 24 60 一个谓词公式的解释可能有很多个 对每一个解释 谓词公式都可以得到一个真值 对公式A中的谓词还可以指派另一组真值 P 1 1 T P 1 2 T P 2 1 F P 2 2 F这是对公式A的另一种解释 在此解释下 公式A的真值为F 对所有的x 1 2 不存在一个y 使P x y T 公式A在D上共有16种解释 2020 3 24 61 3 谓词公式的永真性 定义2 如果谓词公式P对个体域D上的任何一个解释都取得真值T 则称P在D上是永真的 如果P在每个非空个体域上均永真 则称P永真 由定义1可知 要判断一个公式永真 必须对每个个体域上的每一个解释逐一判定 工作量太大 经常是完成不了的 2020 3 24 62 定义3 对于谓词公式P 如果至少存在一个解释使得公式P在此解释下真值为T 则称公式P是可满足的 定义4 如果谓词公式P对于个体域D上的任何一个解释都取得真值F 则称公式P在D上是永假的 如果P在每个非空个体域上均永假 则称P永假 谓词公式的永假性又可称为不满足性或不相容性 2020 3 24 63 4 谓词公式的等价性 定义5 设P与Q是两个谓词公式 D是它们共同的个体域 若对D上的任何一个解释 P与Q都有相同的真值 则称P与Q在D上是等价的 如果D是任意个体域 则称P与Q是等价的 记作 P Q 一些相关的等价式 交换律 P Q Q P结合律 P Q R P Q R 2020 3 24 64 分配律 P Q R P Q P R 德 摩根律 P Q P Q P Q P Q连接词化归律 P Q P Q量词转换律 x P x P x P x P 2020 3 24 65 5 谓词公式的永真蕴含 定义6 对于谓词公式P和Q 如果P Q永真 则称P永真蕴含Q 且称Q为P的逻辑结论 称P为Q的前提 记为 P Q 一些相关的永真蕴含式 假言推理P P Q Q由P Q及P为真 可推出Q为真 拒取式 Q P Q P由P Q及Q为假 可推出P为假 假言三段论P Q Q R P R永真蕴含式是进行演绎推理的重要依据 应用这些公式可确保推理的有效性 因此这些公式又称为推理规则 2020 3 24 66 除此之外 谓词逻辑中还有如下一些推理规则 P规则 在推理的任何步骤上都可引入前提 T规则 推理时 如果前面步骤中有一个或多个公式永真蕴含公式S 则可把S引入推理过程中 反证法 P Q 当且仅当P Q F 即 Q为P的逻辑结论 当且仅当P Q是不可满足的 把反证法推广到谓词公式集 可得到如下反证法定理 定理1 Q为P1 P2 Pn的逻辑结论 当且仅当 P1 P2 Pn Q是不可满足的 2020 3 24 67 从一组已知为真的事实出发 直接运用经典逻辑的推理规则推出结论的过程称为自然演绎推理 基本的推理规则是P规则 T规则 假言推理 拒取式推理等 假言推理P P Q Q由P Q及P为真 可推出Q为真 拒取式 Q P Q P由P Q及Q为假 可推出P为假 P规则 在推理的任何步骤上都可引入前提 T规则 推理时 如果前面步骤中有一个或多个公式永真蕴含公式S 则可把S引入推理过程中 自然演绎推理 2020 3 24 68 这里应避免如下两类错误 一是肯定后件 Q 的错误 另一是否定前件 P 的错误 所谓肯定后件是指 当P Q为真时 希望通过肯定后件Q为真来推出前件P为真 这是不允许的 例1 伽利略在证明哥白尼的日心说时 曾使用了如下推理 1 如果行星系统是以太阳为中心的 则金星会显示出位相的变化 2 金星显出位相变化 3 所以行星系统是以太阳为中心的 这就是使用了肯定后件的推理 违反了经典逻辑的逻辑规则 2020 3 24 69 例2 下面的推理就使用了否定前件的推理 违反了逻辑规则 1 如果下雨 则地上是湿的 2 没有下雨 3 所以地上不湿 这显然是错误的 2020 3 24 70 2 用自然演绎推理求解问题例 已知如下事实 1 凡是容易的课程小王 Wang 都喜欢 2 C班的课程都是容易的 3 ds是C班的一门课程 求证 小王喜欢ds这门课 证明 首先定义谓词 EASY x x是容易的 LIKE x y x喜欢y C x x是C班的一门课 2020 3 24 71 把上述已知事实及待求证的问题用谓词公式表示出来 EASY x LIKE Wang x 凡是容易的课程小王 Wang 都喜欢 x C x EASY x C班的课程都是容易的 C ds ds是C班的一门课程 LIKE Wang ds 小王喜欢ds这门课 待求证问题 2020 3 24 72 应用推理规则进行推理 因为 x C x EASY x 所以 C y EASY y 全称固化因为 C ds C y EASY y EASY ds P规则及假言推理所以 EASY ds EASY x LIKE Wang x LIKE Wang ds T规则及假言推理即 小王喜欢ds这门课程 2020 3 24 73 3 自然演绎推理优缺点优点 表达定理证明过程自然 容易理解 而且其拥有丰富的推理规则 推理过程灵活 便于在其推理规则中嵌入领域启发性知识 缺点 容易产生组合爆炸 推理过程中得到的中间结论一般成指数形式递增 2020 3 24 74 自动定理证明是人工智能的一个重要研究领域 这不仅是由于许多数学问题需要通过定理证明得以解决 而且很多非数学问题 如医疗诊断 机器人行动规划等 也都可归结为一个定理证明问题 定理证明的实质是对前提P和结论Q证明P Q的永真性 但是要证明一个谓词公式的永真性是很困难的 通过研究发现应用反证法的思想可把关于永真性的证明转化为不可满足性的证明 欲证明P Q永真 只要证明P Q不满足就可以了 归结演绎推理 2020 3 24 75 关于不可满足性的证明 海伯伦及鲁宾逊先后进行了卓有成效的研究 提出了相应的理论和方法 海伯伦提出的海伯伦域及海伯伦定理为自动定理的证明奠定了理论基础 鲁宾逊提出的归结原理对机械化推理有了重大的突破 无论是海伯伦还是鲁宾逊的理论 都是以子句集为背景开展研究的 2020 3 24 76 在谓词逻辑中 把原子谓词公式及其否定统称为文字 定义1 任何文字的析取式称为子句 例如 P x Q x P x f x Q x g x 等 定义2 不包含任何文字的字句称为空子句 由于空子句不含有文字 它不能被任何解释满足 所以空子句是永假的 不可满足的 由子句构成的集合称为子句集 在谓词逻辑中 任何一个谓词公式都可通过应用等价关系及推理规则化成相应的子句集 子句 2020 3 24 77 下面给出谓词公式化成子句集的步骤 利用等价关系消去蕴含符号 如 P Q P Q 连接词化规律 例如公式 x y P x y y Q x y R x y 经等价变换后得 x y P x y y Q x y R x y 2020 3 24 78 利用等价关系把否定符号移到每个谓词符号的前面 如 x P x P 量词转换律 P Q P Q 德 摩根律 上式经等价变换后得 x y P x y y Q x y R x y 重新命名变元名 使不同量词约束的变元有不同的名字 上式经等价变换后得 x y P x y z Q x z R x z 2020 3 24 79 用斯柯林 skolem 函数消去存在量词 这里分两种情况 存在量词不出现在全称量词的辖域内 变量y不依赖于其它变量 y用常量A代替 存在量词位于一个或多个全称量词的辖域内 变量y的取值依赖于变量x的取值 此时需要用skolem函数f x1 x2 xn 替换受该存在量词约束的变元 上式中 存在量词 y z 都位于 x 的辖域内 所以都需要用skolem函数替换 设y和z的skolem函数分别为f x 和g x 上式经等价变换后得 x P x f x Q x g x R x g x 2020 3 24 80 把所有的全称量词移到公式的左边 如果公式内部有全称量词 需要把它们都移到公式的左边 上式只有一个全称量词 且已位于公式的最左边 利用等价关系P Q R P Q P R 把公式化为skolem标准形 skolem标准形为 x1 x2 xn M其中 M是子句的合取式 称为skolem标准形的母式 上式经等价变换后得 x P x f x Q x g x P x f x R x g x 2020 3 24 81 消去全称量词 由于此时公式中所有变量都是约束的 全称变量不必要 故可消去 P x f x Q x g x P x f x R x g x 对变元更名 使不同子句中的变元不同名 上式经更名后得到 P x f x Q x g x P y f y R y g y 2020 3 24 82 消去合取词 消去合取词后 上式变为下述子句集 P x f x Q x g x P y f y R y g y 定理2 设有谓词公式F 其标准形的子句集为S 则F不可满足的充要条件是S不可满足 2020 3 24 83 为了判断一个子句的不可满足性 需要对个体域上的一切解释逐个进行判定 只有当该子句对任何非空的个体域上的任何一个解释都是不可满足的 才能判断该子句不可满足 这几乎是不可实现的 对此 海伯伦构造了一个特殊的域 并证明只要对这个特殊域上的一切解释进行判定 就可得知子句集是否不可满足 这个特殊域称为海伯伦域 海伯伦理论 2020 3 24 84 定义3 设S为子句集 则按下述方法构造的域H 称为海伯伦域 简记为H域 1 令H0是S中所有个体常量的集合 若S中不包含个体常量 则令H0 a 其中a为任意指定的一个个体常量 2 令Hi 1 Hi S中所有n元函数f x1 x2 xn xj j 1 2 n 是Hi中的元素 其中i 1 2 2020 3 24 85 例1 求子句集S P x Q x R f y 的H域 解 此例中没有个体常量 故任意指定一个为a 则 H0 a H1 a f a H2 a f a f f a H3 a f a f f f a H a f a f f f a H域求解事例 一 2020 3 24 86 例2 求子句集S P a Q b R f x 的H域解 根据H域的定义 H0 a b H1 a b f a f b H2 a b f a f b f f a f f b H域求解事例 二 2020 3 24 87 例3 求子句集S P a Q f x R g y 的H域解 根据H域的定义得到H0 a H1 a f a g a H2 a f a g a f g a g f a f f a g g a H域求解事例 三 2020 3 24 88 例4 求子句集S P x Q y R y 的H域解 由于该子句集中既无个体常量 又无函数 所以可任意指定一个常量a作为个体常量 从而得到H0 H1 H a H域求解事例 四 2020 3 24 89 基子句 如果用H域的元素代换子句中的变元 则所得的子句为基子句 基原子 基子句中的谓词称为基原子 原子集 子句集中的所有基原子构成的集合称为原子集 子句集S在H域上的解释就是对S中出现的常量 函数及谓词取值 一次取值就是一个解释 下面给出S在H域上解释的定义 2020 3 24 90 定义4 子句集S在H域上的一个解释I满足下列条件 1 在解释I下 常量映射到自身 2 S中的任一个n元函数是Hn H的映射 即 设h1 h2 H 则f h1 h2 hn H 3 S中的任一个n元谓词是Hn T F 的映射 谓词的真值可以指派为T 也可以指派为F 例如 设子句集S P a Q f x 它的H域为 a f a f f a S的原子集为 P a Q f a Q f f a 则S的解释为 I1 P a Q f a Q f f a I2 P a Q f a Q f f a 2020 3 24 91 一般来说 一个子句集的基原子有无限多个 它在H域上的解释也有无限多个 可以证明 对给定域D上的任一个解释 总能在H域上构造一个解释与它对应 如果D域上的解释能满足子句集S 则在H域上的相应解释也能满足S 由此可推出如下两个定理 定理3 子句集S不可满足的充要条件是S对H域上的一切解释为假 定理4 子句集不可满足的充要条件是存在一个有限的不可满足的基子句集S 该定理称为海伯伦定理 2020 3 24 92 海伯伦定理只从理论上给出了证明子句集不可满足性的可行性及方法 但要在计算机上实现其证明过程是很困难的 1965年鲁宾逊提出了归结原理 这才使机器定理证明变为现实 2020 3 24 93 归结原理又称为消解原理 是鲁宾逊提出的一种证明子句集不可满足性 从而实现定理证明的一种理论及方法 由谓词公式转化子句集的过程可以看出 在子句集中子句之间是合取关系 其中只要有一个子句不可满足 则子句集就不可满足 空子句是不可满足的 若一个子句集包含空子句集 则这个子句集一定是不可满足的 鲁宾逊归结原理就是基于这一认识提出来的 鲁宾逊归结推理 2020 3 24 94 基本思想 鲁宾逊归结推理基本思想如下 检查子句集S中是否包含空子句 若包含 则S不可满足 若不包含 就在子句集中选择合适的子句进行归结 一旦通过归结能推出空子句 就说明子句集S是不可满足的 2020 3 24 95 定义5 若P是原子谓词公式 则称P与 P为互补文字 定义6 设C1与C2是子句集中的任意两个子句 如果C1中的文字L1与C2中的文字L2互补 那么从C1与C2中分别消去L1和L2 并将两个子句中余下的部分析取 构成一个新子句C12 则称这一过程为归结 称C12为C1和C2的归结式 称C1和C2为C12的亲本子句 例1 设C1 P Q R C2 Q S这里L1 Q L2 Q 通过归结可得 C12 P R S例2 设C1 P C2 P 通过归结可得 C12 NIL 命题逻辑中的归结推理 2020 3 24 96 例3 设C1 P Q C2 Q R C3 P首先对C1与C2进行归结 得到 C12 P R然后再对C12与C3进行归结 得到 C123 R归结可用一棵树直观的表示出来 如上例可用下图表示其归结过程 2020 3 24 97 定理5 归结式C12是其亲本子句C1与C2的逻辑结论 这是归结原理中很重要的一个定理 由此可得到如下两个推论 推论1 设C1与C2是子句集S中的两个子句 C12是它们的归结式 若用C12代替C1和C2后得到新子句集S1 则由S1的不可满足性可推出原子句集S的不可满足性 即 S1的不可满足性 S的不可满足性 2020 3 24 98 推论2 设C1与C2是子句集S中的两个子句 C12是它们的归结式 若把C12加入S中 得到新子句集S2 则S与S2在不可满足的意义上是等价的 即 S2的不可满足性 S的不可满足性 这两个推论告诉我们 为要证明子句集S的不可满足性 只要对其中可进行归结的子句进行归结 并把归结式加入子句集S 或者用归结式替换它的亲本子句 然后对新子句集证明不可满足性就可以了 如果经过归结能得到空子句 根据空子句的不可满足性 立即可得到原子句集S是不可满足的结论 这就是用归结原理证明子句集不可满足的基本思想 2020 3 24 99 在谓词逻辑中 由于子句中含有变元 所以不像命题逻辑那样可直接消去互补文字 而需要先用最一般合一对变元进行代换 然后才能进行归结 例 设由如下两个子句 C1 P x Q x C2 P a R y 由于P x 与P a 不同 所以C1与C2不能直接进行归结 但若用最一般合一 a x 对两个子句分别进行代换 C1 P a Q a C2 P a R y 就可对他们进行归结 消去P a 与P a 得到如下的归结式 Q a R y 谓词逻辑中的归结推理 2020 3 24 100 下面给出谓词逻辑中关于归结的定义 定义7 设C1与C2是两个没有相同变元的子句 L1和L2分别是C1和C2中的文字 若 是L1和 L2的最一般合一 则称 C12 C1 L1 C2 L2 为C1和C2的二元归结式 L1和L2称为归结式上的文字 2020 3 24 101 例1 设C1 P a Q x R x C2 P y Q b 1 若选L1 P a L2 P y 则 a y 是L1与L2的最一般合一 根据 定义7 可得 C12 C1 L1 C2 L2 P a Q x R x P a P a Q b P a Q x R x Q b Q x R x Q b Q x R x Q b 2020 3 24 102 2 若选L1 Q x L2 Q b b x 则可得 C12 P a Q b R b Q b P y Q b Q b P a R b P y P a R b P y P a R b P y 2020 3 24 103 例2 设C1 P x Q a C2 P b R x 由于C1与C2有相同的变元 不符合 定义7 的要求 为了进行归结 需修改C2中变元的名字 令C2 P b R y 此时L1 P x L2 P b L1与L2的最一般合一 b x 则 C12 P b Q a P b P b R y P b Q a R y Q a R y 2020 3 24 104 Attention 1 如果在参加归结的子句内部含有可合一的文字 则在进行归结之前应对这些文字先进行合一 2 对于谓词逻辑 定理4 仍然适用 即归结式是它的亲本子句的逻辑结论 用归结式取代它在子句集S中的亲本子句所得的新子句集仍然保持着原子句集S的不可满足性 3 对于一阶谓词逻辑 从不可满足的意义上说 归结原理也是完备的 即若子句集是不可满足的 则必然存在一个从该子句集到空子句的归结演绎 若从子句集存在一个到空子句的演绎 则该子句集是不可满足的 2020 3 24 105 归结原理给出了证明子句集不可满足性的方法 根据 定理1 如欲证明Q为P1 P2 Pn的逻辑推论 只需证明 P1 P2 Pn Q是不可满足的 再根据 定理2 公式 P1 P2 Pn Q的不可满足性与其子句集的不可满足性是等价的 因此我们可用归结原理来进行定理的自动证明 应用归结原理证明定理的过程称为归结反演 设F为已知前提的公式集 Q为目标公式 结论 归结反演 2020 3 24 106 归结反演证明 用归结反演证明Q为真的步骤是 1 否定Q 得到 Q 2 把 Q并入到公式集F中 得到 F Q 3 把公式集 F Q 化为子句集S 4 应用归结原理对子句集S中的子句进行归结 并把每次归结到的归结式都并入S中 如此反复进行 若出现了空子句 则停止归结 此时就证明了Q为真 2020 3 24 107 例1 已知 F1 x N x GZ x I x 自然数都是大于零的整数 F2 x I x E x O x 所有整数不是偶数就是奇数 F3 x E x I S x 偶数除以2是整数 求证 所有自然数不是奇数就是其一半为整数的数 证明 首先把要证明的问题用谓词公式表达出来 G x N x O x I S x 把F1 F2 F3及G化成子句集 1 N x GZ x 2 N u I u 3 I y E y O y F2 4 E z I S z F3 5 N t 6 O t G 7 I S t 对子句进行归结 8 I y E y 3 与 6 归结 y t 9 E z 4 与 7 归结 z t 10 I y 8 与 9 归结 y z 11 N u 2 与 10 归结 u y 12 NIL 5 与 11 归结 u t 所有自然数不是奇数就是其一半为整数的数 2020 3 24 108 上述过程可用如下归结树表示 2020 3 24 109 例2 某公司招聘工作人员 A B C三人应试 经面试后公司表示如下想法 1 三人中至少录取一人 2 如果录取A而不录取B 则一定录取C 3 如果录取B 则一定录