经典逻辑推理学习ppt课件

第 章经典逻辑推理 基本概念 自然演绎推理 归结演绎推理 与 或形演绎推理 基本概念 何为推理 从已知的事实出发 不断运用已掌握的 知识库中的 知识推出或归纳出新的事实 包括目标结论 的过程称为推理 人工智能中推理是由程序实现的 称这个程序为推理机 推理方式及其分类 人工智能作为对人类智能的模拟 有多种推理方式 它们是 演绎推理 归纳推理 默认推理 确定性推理 不确定性推理 单调推理 非单调推理 启发式推理 非启发式推理 基于知识的推理 统计推理 直觉推理 分别解释如下 演绎推理 归纳推理 默认推理 所谓演绎推理是从全称判断推导出特称判断的过程 是从一般到个别的推理 经常用的是三段论式 它包括 大前提 已知的一般性知识或假设 小前提 具体情况或个别事实 结论 由大前提推出的适合小前提所示情况的新判断 演绎推理 归纳推理 默认推理 例如有如下三个判断 足球运动员的身体都是强壮的 高波是一名足球运动员 所以 高波的身体是强壮的 其中 是大前提 是小前提 是经演绎推出的结论 只要大前提和小前提是正确的 那麽由它们推出的结论就是正确的 演绎推理 归纳推理 默认推理 演绎推理是人工智能中的一种重要推理方式 目前研制成功的各类智能系统中 大多是用演绎推理实现的 演绎推理 归纳推理 默认推理 归纳推理是从足够多的事例中归纳出一般性结论的推理过程 是一种从个别到一般的推理 例如 某厂进行产品质量检查 如果对每一件产品都进行了检查 并且都是合格的 则推导出结论 该厂生产的产品是合格的 并称这种推理为完全归纳推理 演绎推理 归纳推理 默认推理 如果是随机地抽查部分产品 并且它们是合格的 则得出结论该厂的产品是合格的 这种推理称为不完全归纳推理 默认推理又称为缺省推理 它是在知识不完全的情况下假设某些条件已经具备所进行的推理 例如 在条件 已成立的情况下 如果没有足够的证据能证明条件 不成立 则默认 成立 并在默认前提下进行推理 推导 演绎推理 归纳推理 默认推理 出某个结论来 由于这种推理允许默认某些条件是成立的 这就摆脱了需要知道全部有关事实才能进行推理的要求 使得在知识不完全的情况下也能进行推理 在默认推理过程中 如果到某一时刻发现原先所做的默认不正确 则可以撤消默认推理和所推出的结论 并重新按新情况进行推理 确定性推理 不确定性推理 所谓确定性推理是指推理时所用的知识都是精确的 推出的结论也是确定的 是真或者是假 经典逻辑推理就属于这一种 不确定性推理是指推理时所用的知识不都是精确的 推出的结论也不完全是肯定的 其真值位于真与假之间 命题的外延模糊不清 确定性推理 不确定性推理 这里 我们特别强调的是不确定性推理 因为 人类思维活动的特征经常是在知识不完全的情况下进行多方位的思考及推理的 因此 要使计算机模拟人类的思维活动 就必须使它具有不确定性推理的能力 单调推理 非单调推理 所谓单调推理是指在推理的过程中随着推理的向前推进及新知识的加入 推出的结论是单调递增的趋势 并且越来越接近目标 推理过程不会出现反复的情况 即不会因新知识的加入否定了前面推出的结论 从而使推理又退回到前面的某一步 经典逻辑演绎推理属于这一种 启发式推理 非启发式推理 若按推理中是否使用与问题有关的启发性知识 推理可分为启发式推理和非启发式推理 所谓启发性知识是指与问题有关并且能加快推理进程 求得问题最优解的知识 基于知识的推理 统计推理 直觉推理 如果从方法论的角度来划分 推理可分为基于知识的推理 统计推理和直觉推理 顾名思义 所谓基于知识的推理就是根据已掌握的事实 通过运用知识进行推理 统计推理是根据对某事物的数据统计进行推理 例如 对农作物的产量进行统计 从而得出是否增产的结论 从而找 基于知识的推理 统计推理 直觉推理 出增产和减产的原因 就是运用了统计推理 直觉推理又称常识性推理 是根据常识进行的推理 例如 当你从某建筑物下走过时 猛然发现有一物体坠落 这时你立即就会意识到这有危险 并立即躲开 这就是使用了直觉推理 目前直觉推理在计算机上的实现还是一件很困难的工作 推理的控制策略 推理的控制策略主要包括推理方向 搜索策略 冲突消解策略 求解策略及限制策略等 推理方向用于确定推理的驱动方式 分为正向推理 逆乡向推理 混合推理及双向推理四种 正向推理 正向推理也称数据驱动推理 前向链推理 模式制导推理及前件推理等 正向推理过程的算法描述如下 将用户提供的初始已知事实送入数据库DB 2 检查数据库DB中是否包含问题的解 若有则求解结束 成功退出 否则执行下一步 正向推理 根据数据库DB中的已知事实 扫描知识库KB 检查KB中是否有可适用的知识 若有则转 否则转 把KB中所有的适用知识都选出来 构成可适用的知识集KS 若KS不空 则按某种冲突消解策略从中选出一条知识进行推理 并将推出的新事实加入DB中 然后转 若KS空 转 正向推理 询问用户是否可以进一步补充新的事实 若可补充 则将补充的事实加入DB中 转 否则表示求不出解 失败退出 算法的流程示意图如 115的图 所示 为了实现正向推理 还有很多实际问题需要解决 后面将陆续介绍 逆向推理 逆向推理的思想是首先假设一个目标 然后寻找支持该假设的证据 若所需的证据都能找到 则说明假设是成立的 若实在找不到证据时 说明原假设不成立 此时需另做假设 推理过程的算法如下所示 逆向推理 提出要求证的目标 假设目标 检查该目标是否已在数据库中 若在 则该目标成立 成功退出或者对下一目标进行检验 否则 转下一步 判断该目标是否是证据 即它是否是由用户证实的原始事实 若是 则询问用户 否则转下一步 在知识库中找出所有能导出该目标的知识 形成适用知识集KS 转下一步 逆向推理 从KS中选出一条知识 并将该知识的运用条件作为新的假设目标 然后转 算法的示意图如 116的图 所示 双向推理 混合推理就是在推理过程中合理地使用正向推理和逆向推理 混合推理的算法示意图如P11 的图 所示 求解策略和限制策略 所谓推理的求解策略是指只求一个解还是求所有解和最优解等 为了防止无穷的推理过程 以及由于推理过程太长增加时间及空间的复杂性 可在控制策略中指定推理的限制条件 以对推理的深度 宽度 时间 空间等限制 模式匹配 模式匹配是推理中必须进行的一项重要工作 因为只有经过模式匹配才能从知识库中选出当前适用的知识 才能进行推理 模式匹配可以有确定性匹配和不确定性匹配良种 所谓确定性匹配是指两个模式完全一样 或者通过代换后变得完全一致 所谓不确定性匹配是指两个知识模式不完全一样 但从总体上看它们的相似程度又落在规定的限度内 无论是确定性匹配还是不确定性匹配都需要进行变量的代换 模式匹配 例如设有如下两个知识模式 1 father 李四 李小四 andman 李小四 2 father x y andman y 若用李四代换x 用李小四代换y 则 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 则不是一个代换 因为代换的目的是使某些变元被另外的变元 常量 或函数表达式取代 使之不再在公式中出现 而 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 模式匹配 下面给出一个公式的代换例式的概念 设F是一个公式 是一个代换 记F 为公式F在 下的代换例式 它是将公式F中的变量用 中的项作代换的结果 例如有公式 x y f y 和代换 a x b y 于是F a b f b 模式匹配 下面给出复合代换的定义设有两个代换 和 其中 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 xi时ui yi当yi x1 x2 xn 时 后剩下的元素构成的集合 记为 模式匹配 例如设有如下代换 f y x z y a x b y y z 求 和 解 我们先来求 模式匹配 f y x z y a x b y y z f b x y y a x b y y z 去掉不合法的元素 y y 条件 a x b y 条件 于是 f b x y z 模式匹配 再来求 同样先求 a x b y y z f y x z y a x b y z z f y x z y 去掉不合法的元素z z f y x z y得 a x b y 显然代换的复合运算是不可交换的 并且对任何代换 存在空代换 并且 模式匹配 下面我们给出合一的概念 设有公式集F F1 F2 Fn 若存在一个代换 使得F1 F2 Fn 则称 为公式集F的一个合一 且称F1 F2 Fn是可合一的 模式匹配 例如F P x y a x g a y 求公式F在 下的例式为F P a g a 对于公式集F P x y f y P a g x z 则 a x g a y f g a z 是公式F的一个合一 模式匹配 一个公式的合一一般是不唯一的 但如果 是公式集F的一个合一 若对任一个合一 都存在一个代换 使得 则称 是一个最一般合一 模式匹配 最一般合一是唯一的 若用最一般合一去代换那些可合一的谓词公式 可使它们变成完全一致的公式 由此可知 为了使两个知识模式匹配 可用其最一般合一对它们进行代换 模式匹配 为了求最一般合一要用到一个差异集 也有叫分歧集的 的概念 设有如下两个谓词公式F1 P x y z F2 P x f a h b 分别从F1与F2的第一个符号开始 逐个向右比较 此时发现F1中的y与F2中的f a 不同 它们构成了一个差异集 D1 y f a 模式匹配 当继续向右比较时 又发现F1中与F2中的h b 不同 于是又得到一个差异集 D2 z h b 下面给出求最一般合一的算法 1 令K 0 Fk F k 这里 F是欲求其最一般合一的公式集 是空代换 它表示不做代换 2 若Fk只含一个表达式 则算法停 k就是所求最一般合一 模式匹配 3 找出Fk的差异集Dk 4 若Dk中存在元素xk和tk 其中xk是变元 tk是项 且xk不在tk中出现 则置 k 1 k tk xk Fk 1 Fk tk xk K k 1转 2 5 算法停 F的最一般合一不存在 模式匹配 例如 设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 0 a z F1 P a x f g y P a f a f u 模式匹配 4 D1 x f a 5 2 1 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 2 g y u a z f a x g y u 模式匹配 8 F3 F2 g y u P a f a f g y P a f a f g y u P a f a f g y 因为F3只含一个表达式了 所以 3就是最一般合一 即 a z f a x g y u 是最一般合一 冲突消解策略 接下来我们学习冲突消解方面的概念 在推理的过程中 系统不断的用以知的事实与知识库中的知识进行匹配 此时可能发生如下三种情况 1 已知事实不能与知识库中的任何知识匹配成功 2 已知事实恰好与知识库中的一条知识匹配成功 冲突消解策略 3 已知事实可与知识库中的多条知识匹配成功 以上三种情况中 第一种情况使得推理无法进行下去 第三种情况则出现冲突 需要按一定的策略解决冲突 冲突消解策略 目前解决冲突的策略有多种 其基本思想都是对知识进行排序 常用的有以下几种 1 按针对性排序设有如下两条产生式规则 r1 IFA1andA2and AnTHENH1r2 IFB1andB2and BmTHENH2 冲突消解策略 如果存在最一般合一 使得r1中每一个Ai都可变成相应的Bi 即r2中除了包含r1的全部条件A1 A2 An外 还包含其它条件 则称r2比r1有更大的针对性 r1比r2有更大的通用性 一般选用针对性较强的产生式规则 即应选用r2 因为它要求的条件较多 其结论一般更接近目标 一旦得到满足 可缩短推理过程 冲突消解策略 2 按已知事实的新鲜性排序在产生式系统推理过程中 每应用一条产生式规则就会得到一个或多个结论 数据库就会增加新的事实 把数据库后生成的事实称为新鲜的事实 即后生成的事实比先生成的事实具有较大的新鲜性 设规则r1可与事实组A匹配成功 规则r2可与事实组B匹配成功 则A与B中哪一组新鲜与它匹配的产生式规则就先被应用 冲突消解策略 3 按匹配排序在不确定性匹配中 为了确定两个知识模式是否可以匹配 需要计算这两个模式的相似程度 当其相似程度达到某个预定的值时 就认为它们是可匹配的 若两条规则均按匹配度匹配成功 则匹配度大的那条规则优先启用 冲突消解策略 4 根据领域问题的特点排序某些领域问题可事先知道它的某些特性 可根据这些特性把知识排成固定的顺序 先匹配成功的优先启用的原则 冲突消解策略 5 按上下文限制排序把产生式规则按它们所描述的上下文分成若干组 在不同的条件下 只能从相应的组中选取有关的产生式规则 这样可以减少冲突的发生 冲突消解策略 6 按冗余限制排序若哪一条产生式规则被应用后产生冗余知识 则就降低它被应用的优先级 7 按条件个数排序如果有多条产生式规则生成的结论相同 则要求条件少的产生式规则被优先应用 4 2自然演绎推理 从一组已知的事实出发 直接运用经典逻辑推理规则推出结论的过程称为自然演绎推理 其中 基本的推理规则是P规则 T规则 假言推理 拒取式推理等 假言推理的一般形式是P P Q Q拒取式的一般形式是P Q Q P 4 2自然演绎推理 以下是自然演绎推理的例子 例1 A B A C B C D D Q Q1 AP规则2 A CP规则3 CT规则1和24 BP规则5 B CT规则3和4 4 2自然演绎推理 6 B C DP规则7 DT规则5和68 D QP规则9 QT规则7和8问题得证 4 2自然演绎推理 例2设已知如下事实 1 凡是容易的课程小王 Wang 都喜欢 2 C班的课程都是容易的 3 ds是C班的一门课程求证小王喜欢ds这门课程 4 2自然演绎推理 证明 首先定义谓词如下 Easy x x是容易的Like x y x喜欢yC x x是C班的一门课程于是问题可以表示成 4 2自然演绎推理 x Easy x Like Wang x x C x Easy x C ds Like Wang ds 4 2自然演绎推理 1 x Easy x Like Wang x P规则2 Easy ds Like Wang ds US规则和13 x C x Easy x P规则4 C ds Easy ds US规则和35 C ds Like Wang ds T规则2和46 C ds P规则7 Like Wang ds T规则5和6即小王喜欢ds这门课程 4 2自然演绎推理 自然演绎推理的优点是表达定理证明过程自然 容易理解 拥有丰富的推理规则 推理过程灵活 便于在推理过程中嵌入领域启发知识 缺点是容易产生组合爆炸 推理过程中得到的中间结论一般呈指数形式递增 这对于一个大型推理问题是十分不利的 甚至是不可能实现的 4 3归结演绎推理 定理证明是人工智能的一个重要研究领域 这不仅仅是因为许多数学问题要通过定理证明得以解决 很多非数学问题 如医疗诊断 机器人规划及难题求解等 也都归结为一个定理证明问题 定理证明的实质是对前提P和结论Q证明P Q的永真性 但是证明一个谓词公式的永真性不像证明一个命题公式的永真性那麽简单 它牵涉到谓词变量 客体变量及函数符号 在某些情况下甚至是行不通的 4 3归结演绎推理 在这种情况下 人们提出了用反证法来解决问题的思路 在这方面 海伯伦和鲁宾逊都作出了杰出的贡献 两人的研究都是以子句集为背景展开的 接下来 我们介绍这些概念 4 3归结演绎推理 子句 在谓词逻辑中 称原子谓词公式及其否定为文字 任何文字的析取式为子句 例如 P x Q x P x f x Q x g x 都是子句 而P x Q x g x P x f x 等都是文字 并把不包含任何文字的子句称为空子句 4 3归结演绎推理 由于空子句不包含任何文字 它不能被任何解释所满足 所以空子句是永假的 不可满足的 由子句构成的集合称为子句集 在谓词逻辑中任何一个谓词公式均可通过等价变换化为相应的子句集 4 3归结演绎推理 化子句集的步骤如下 1 利用等价公式消去公式中的逻辑连接词 和 P Q P QP Q P Q P Q 4 3归结演绎推理 2 利用下列公式将否定符号 深入到单个变元前 P P P Q P Q P Q P Q x P x P x P x P 4 3归结演绎推理 3 重新命名变元名 使不同量词约束的变元有不同的名字4 消去存在量词 分两种情况处理 一种情况是存在量词不出现在全称量词的辖域内 此时只要用一个新的个体常量替换受该存在量词约束的变元就可消去存在量词 另一种情况是存在量词位于一个或多个全称量词的辖域内 例如 x1 x2 xn y P x1 x2 xn y 此时需要用Skolem函数f x1 x2 xn 替换受该存在量词约束的变元 然后才能消去存在量词 4 3归结演绎推理 5 把全称量词全部移到公式的左边 6 利用等价关系P Q R P Q P R 把公式化为Skolem标准型 4 3归结演绎推理 Skolem标准型的一般形式是 x1 x2 xn M其中 M是子句的合取式 称为Skolem标准型的母式 7 消去全称量词8 对变元更名 使不同子句中的变元不同名 4 3归结演绎推理 9 消去合取连接词 变为子句集 子句集中各子句之间是合取关系 谓词公式是不可满足的 则其子句集合是不可满足的 反之亦然 海伯伦理论 如何证明一个子句集是不可满足的呢 下面就海伯伦理论和鲁宾逊的归结原理进行讨论 一 海伯伦理论要判定一个子句集是否是不可满足的 需要对子句集中的谓词公式进行判定 而谓词公式的判定需要对个体域上的任何解释进行判定 这是很困难的 海伯伦理论 海伯伦定义了一个特殊的域称为海伯伦域 在任何域上的判定 只要在海伯伦域上进行即可 设S是子句集 则按下述方法构造的域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 0 1 下面通过例子来解释这个定义 海伯伦理论 例1求子句集S P x Q x R f y 的H域 解 因为S中没有个体常量 所以指定a作为个体常量 于是得到 H0 a H1 a f a H2 a f a f f a H a f a f f a f f f a H a f a f f a 海伯伦理论 例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 海伯伦理论 例3 求子句集S P x Q y R y 的H域 解 由于该子句集中既无个体常量 又无函数 所以可任意指定一个常量a作为个体常量 从而得到H0 H1 H a 有定理说 子句集S是不可满足的充要条件是S对H域上的一切解释都为假 并且海伯伦证明了若子句集S在任何域D上的解释能满足S 则在H域上相应的解释也能满足S 下面我们说明 S在H域上解释的定义 海伯伦理论 子句集S在H域上的一个解释满足下列条件 1 在解释I下 常量映射到自身 2 S中的任一个n元函数是Hn H的映射 即 设h1 h2 hn H 则f h1 h2 hn H 海伯伦理论 3 S中的任一n元谓词是Hn T F 的映射 即谓词的真值可以指派T也可指派F 海伯伦在理论上证明了子句集不可满足性的可行性及方法 但要在计算机上实现其证明过程还是很困难的 1965年鲁宾逊提出了归结原理 使机器证明成为现实 鲁宾逊归结原理 归结原理也称消解原理 是鲁宾逊提出的一种证明子句不可满足性 从而实现定理证明的一种理论及方法 由谓词公式转化为子句集的过程可以看出 在子句集中子句之间的关系是合取关系 其中只要有一个子句不可满足 则子句集就不可满足 前面 我们曾经说过空子句是不可满足的 即一个子句集中若含空子句 则它是不可满足的 鲁宾逊归结原理 归结原理的基本思想就是检查子句集中是否含空子句 若含 则子句集S不可满足 或说证明一个谓词公式是永假的过程 就是归结由此公式转换成的子句集包含空子句的过程 鲁宾逊归结原理 下面我们先来说明命题逻辑中的归结原理定义P是原子谓词公式 则称P与 P为互补文字 我们知道在命题逻辑中有公式 P Q Q R P R即 P Q Q R P Rc1c2c12 鲁宾逊归结原理 显然上述公式向我们展示的是在子句c1中存在文字Q 在子句c2中存在Q的补文字 Q 把这一对互补文字消去 剩下的文字析取起来就是子句c1和c2的逻辑结果c12 并称c12是c1和c2的归结式 c1和c2则称为c12的亲本子句 鲁宾逊归结原理 例如 1 C1 P Q RC2 Q S它们的归结式c12为 P R S2 C1 PC2 P它们的归结式c12为NIL即空子句 鲁宾逊归结原理 3 C1 P QC2 Q RC3 P它们的归结式c123为R 其归结过程可以用下面的一个树形结构很清楚的表现出来 鲁宾逊归结原理 P Q Q R P RPR归结过程的树形表示图 鲁宾逊归结原理 由命题逻辑中的归结原理可以得出如下的推论 设c1与c2是子句集S中的两个子句 c12是它们的归结式 若用c12代替c1和c2后得到新子句集S1 则由S1的不可满足性可以推出S的不可满足性 这个定理告诉我们 证明子句集S的不可满足性问题 可以转化成证子句集S1的不可满足性问 直到从子句集Sn中推出一个空子句来 鲁宾逊归结原理 在谓词逻辑中 由于子句中含有变元 所以不象命题逻辑中那样可以直接消去互补文字 而先要用最一般合一对变元进行代换 然后才能进行归结 前面我们已经介绍过最一般合一的概念 下面给出谓词逻辑中二元归结式的概念 鲁宾逊归结原理 设C1与C2是两个没有公共变量的子句 L1和L2分别是C1与C2中的文字 若 是L1和 L2的最一般合一 则称C12 C1 L1 C2 L2 为C1与C2的二元归结式 L1和L2称为归结式上的文字 例子见P132页的例4 10和例4 11 鲁宾逊归结原理 例如设C1 P a Q x R x C2 P y Q b 若选L1 P a L2 P y 则 a y 是L1与 L2的最一般合一 于是有C12 C1 L1 C2 L2 Q x R x Q b Q x R x Q b 鲁宾逊归结原理 若选L1 Q x L2 Q b 则 b x 是L1与 L2的最一般合一 于是有C12 C1 L1 C2 L2 Q x R x Q b P a R b P y 鲁宾逊归结原理 再例如设有如下子句 1 P x Q a 2 P b R x 由于 1和 2有相同的变元不符合二元归结式中定义中对子句 1和 2的要求 为了归结的需要 要修改 2中变元的名字 鲁宾逊归结原理 令 2 P b R y 此时 1 P x 2 P b 它们的最一般合一为 b x 于是有C12 P b Q a P b P b R y P b Q a R y 如果在参加归结的子句内部有可合一的文字 则在归结之前应先对这些文字合一 见下例 鲁宾逊归结原理 设有子句 C1 P x P f a Q x C2 P y R b 由于在C1中有可合一文字P x 和P f a 若用它们的最一般合一 f a x 进行代换 得到C1 P f a Q f a 此时可对C1 和C2进行归结 从而的到C1和C2的二元归结式 对C1 和C2分别选 1 P f a 2 P y 它们的最一般合一是 鲁宾逊归结原理 f a y 于是可得它们的归结式为 C12 b Q f a 上例中称C1 为C1因子 如果C1 是一个单文字 则称它为C1的单元因子 应用因子的概念 可对谓词逻辑中的归结原理给出如下的定义 鲁宾逊归结原理 定义 子句 1和 的归结式是下列二元归结式之一 1 1和 的二元归结式 2 1和 的因子 2的二元归结式 3 的因子 1 1和 的二元归结式 4 1的因子 1 1和 的因子 2的二元归结式 鲁宾逊归结原理 在谓词逻辑中仍然有 归结式是它的亲本子句的逻辑结果 用归结式代替子句集 中的亲本子句所得到的新子句集 仍然保持子句集 的不可满足性 归结反演 归结反演原理 欲证P1 P2 Pn Q 1 P1 P2 Pn Q T 2 P1 P2 Pn Q T 3 P1 P2 Pn Q F 4 我们的工作过程是从后向前进行的 即证 4 就是证明了 3 证 3 就是证明了 2 证 2 就是证明了 1 归结反演 在使用消解过程之前 我们必须把任一谓词公式转换成子句 下面给出转化过程的步骤 1 消去单条件运算符号 应用公式A B A B 2 将否定符号深入到单个谓词变元的前面 利用公式 A B A B A B A B x A x x A x x A x x A x 归结反演 3 对变量标准化在任一量词辖域内 受该量词约束的变量为一哑元 虚构变量 它可以在该辖域内处处统一地被另一个没有出现过的任一变量所代替 而不改变公式的真值 合适公式中变量的标准化意味着对哑元改名以保证每个量词有其自己唯一的哑元 例如把 x A x x B x 标准化为 x A x y B y 归结反演 4 消去存在量词在公式 x y P x y 中 存在量词是在全称量词的辖域内 我们允许所存在的x可能依赖于y值 令这种依赖关系明显地由函数g y 所定义 它把每个y值映射到存在的那个x 这种函数叫做skolem函数 如果用skolem函数代替存在的x 我们就可以消去全部存在量词 并写成 y P g y y 归结反演 在公式 x y P x y 中 存在量词是在全称量词的辖域内 我们允许所存在的x可能依赖于y值 令这种依赖关系明显地由函数g y 所定义 它把每个y值映射到存在的那个x 这种函数叫做skolem函数 如果用skolem函数代替存在的x 我们就可以消去全部存在量词 并写成 y P g y y 归结反演 从一个公式消去存在量词的一般规则是以一个skolem函数代替每个出现的存在量词的量化变量 而这个skolem函数的变量就是由那些全称量词所约束的全称量词量化变量 这些全称量词的辖域包括要被消去的存在量词的辖域在内 skolem函数所使用的函数符号必须是新的 即不允许是公式中已经出现过的函数符号 例如 y x P x y 被 y P g y y 代替 其中g y 为一skolem函数 归结反演 如果要消去的存在量词不在任何一个全称量词的辖域内 那麽我们就用不含变量的skolem函数即常量 例如 x P x 化为P A 其中常量符号A用来表示我们知道的存在实体 A必须是个新的常量符号 它未曾在公式中其它地方使用过 归结反演 5 化为前束形到这一步已不留下任何存在量词 而且 每个全称量词都有自己的变量 把所有全称量词移到公式的左边 并使每个量词的辖域包括这个量词后面公式的整个部分 所得公式称为前束形 归结反演 前束形公式由前缀和母式组成 前缀由全称量词组成 母式由没有量词的公式组成 即前束形 前缀 母式 全称量词串无量词公式 归结反演 6 把母式化为合取范式任何母式都可写成由一些谓词公式和 或 谓词公式的否定的析取的有限集组成的合取 这种母式叫做合取范式 我们可以反复应用 对 的分配律 把任一母式化成合取范式 例如 A B C A B A C 归结反演 7 消去全称量词到了这一步 所有余下的量词均被全称量词量化了 同时 全称量词的次序已经不重要了 于是我们可以消去全称量词 归结反演 8 消去连接词符号 用A B代替A B 这样反复代替的结果 最后得到一个有限集 其中每个公式是文字的析取 任一个只由文字的析取构成的合式公式叫做一个子句 9 更换变量名称可以更换变量符号的名称 使一个变量符号不出现在一个以上的子句中 下面我们用例子来说明化子句并进行消解的过程 归结反演 例1试证 G是F1和F2的逻辑结论 其中F1 x P x y Q y L x y F2 x P x y R y L x y G x R x Q x x P x y Q y L x y x P x y R y L x y x R x Q x 归结反演 证明 首先把F1 F2和 G转化成子句形 F1 x P x y Q y L x y x P x y Q y L x y x y P x Q y L x y P x Q y L x y 归结反演 F2 x P x y R y L x y x P x y R y L x y P a y R y L a y y P a R y L a y P a R z L a z 归结反演 G x R x Q x x R x Q x R x Q x R b Q b 得到子句集合如下 1 P x Q y L x y 2 P a 3 R z L a z S4 R b 5 Q b 归结反演 6 Q y L a y 1和2及 a x 7 L a b 5和6及 b y 8 R b 3和7及 b z 9 4和8及 即S是不可满足的 G是F1和F2的逻辑结论 归结反演 例2 已知 任何人的兄弟不是女性 任何人的姐妹必是女性 Mary是Bill的姐妹 试用归结推理的方法证明Mary不是Tom的兄弟 解 为了求解此问题首先定义如下谓词 brother x y x是y的兄弟 sister x y x是y的姐妹 woman x x是女性 归结反演 于是问题可以描述成 x y brother x y woman x x y sister x y woman x sister Mary Bill brother Mary Tom 归结反演 首先将前提和结论的否定转换成子句形 x y brother x y woman x brother x y woman x x y sister x y woman x sister x y woman x brother Mary Tom brother Mary Tom sister Mary Bill 归结反演 整理得子句集合S如下 1 sister Mary Bill 2 brother Mary Tom S3 brother x y woman x 4 sister z w woman z 归结反演 5 woman Mary 和3及 Mary x Tom y 6 woman Mary 1和4及 Mary z Bill w 7 5和6及空代换 问题得证 归结反演 例3 已知 John是贼 Paul喜欢酒 wine Paul也喜欢奶酪 cheese 如果Paul喜欢某物则John也喜欢某物 如果某人是贼 并且他喜欢某物 则他很可能会偷窃该物 试用归结推理的方法证明John可能偷窃了什麽 归结反演 解 为了求解该问题定义如下谓词 thief x x是贼like x y 某人x喜欢某物ymay steal x y 某人x可能偷窃了某物y 归结反演 于是问题可以描述成 thief John like Paul wine like Paul cheese y like Paul y like John y x thief x y like x y may steal x y may steal John Z 归结反演 首先把前提和结论的否定转换成子句形 y like Paul y like John y like Paul y like John y x thief x y like x y may steal x y thief John y like John y may teal John y y thief John like John y may steal John y thief John like John y may steal John y may steal John Z 整理得子句集合S为 1 thief John 2 like John y may steal John y 3 like Paul wine 4 like Paul cheese 5 may steal John Z 6 like Paul X like John X 7 like John wine 3和6及 wine x 8 may steal John wine 2和7及 wine y 9 5和8及 问题得证 应用归结原理求取问题的答案 利用归结原理还可以来求取问题的答案 思想与定理证明类似 其求解步骤如下 把已知前提用谓词公式表示出来 并且化为相应的子句集 把待求解的问题也用谓词公式表示出来 然后把它否定并与谓词ANSWER构成析取式 ANSWER是一个为了求解问题而专设的谓词 其变元必须与待求解问题公式的变元完全一致 应用归结原理求取问题的答案 把析取式化为子句集 并且把该子句并入到子句集 中 得到子句集合 对 应用归结原理进行归结 若得到归结式ANSWER 则答案就在ANSWER中 应用归结原理求取问题的答案 例 1 已知王 wang 先生是小李 li 的老师 2 小李与小张 zhang 是同班同学 3 如果x与y是同班同学 则x的老师也是y的老师 求小张的老师是谁 应用归结原理求取问题的答案 解 首先定义谓词 T x y x是y的老师 C x y x与y是同班同学 把已知前提和待求解的问题表示成谓词公式 F1 T wang li F2 C li zhang F3 x y z C x y T z x T z y 应用归结原理求取问题的答案 G x T x zhang ANSWER x 把上述公式化为子句集 1 T wang li 2 C li zhang S 3 C x y T z x T z y 4 T u zhang ANSWER u 应用归结原理求取问题的答案 应用归结原理进行归结 5 C li y T z y 1 和 3 归结 6 C li zhang ANSWER wang 4 5 7 ANSWER wang 2 与 6 归结其归结树如 137的图 9所示 应用归结原理求取问题的答案 例 设 B C三人中有人从不说真话 也有人从不说假话 某人向这三人分别提出同一个问题 谁是说谎者 答 和 是说谎者 答 和 是说谎者 答 和 中至少有一个说谎者 求谁是诚实的人 谁是说谎者 应用归结原理求取问题的答案 解 令T x 表示x说真话如果 说的是真话 则有T A T B T C 如果 说的是假话 则有 T A T B T C 对 和 说的话做相同的处理得 T T T C T T T C 应用归结原理求取问题的答案 T T T B T C T T B 把上面的公式化为子句集 得 1 T T B 2 T T C 3 T B T C 4 T T T C 5 T T T B 6 T T C 应用归结原理求取问题的答案 7 T B T C 下面首先求谁是老实人 把 T x ANSWER x 并入 得 1 8 T x ANSWER x 在 1上进行归结得 9 T A T C 1 和 7 应用归结原理求取问题的答案 10 T C 6 和 9 11 ANSWER C 8 和 10 及 C x 即 是老实人 由于对 1进行归结得不出ANSWER 和ANSWER 所以下面来证明 和 不是老实人 设 不是老实人 则有 T 把它的否定并入 中得 2 应用归结原理求取问题的答案 即 2只比 多了一个子句 8 T 9 T T C 1 和 7 10 T 2 和 9 11 NIL 8 和 10 所以 不是老实人 同理可证 不是老实人 归结策略 实际用计算机进行归结时使用的是水平浸透法 即对 中的每一对子句进行比较 有归结式即产生直到推出一个空子句 从上面的例子我们可以看出影响归结效率的重要因素是子句的数量和子句中文字的数量 下面我们给出一些提高归结效率的方法 归结策略 要想提高消解效率 当然是希望子句集合S中的子句越少越好 子句中的文字越少越好 为了提高消解效率 人们提出了很多控制策略 例如 删除策略 线性归结 单元归结 输入归结等 删除策略 所谓删除策略是指 若子句集合S中有永真式则直接可以删除 因为它不影响子句集合S的不可满足性 此外被前面子句归类的子句也可以被删除 下面给出归类的概念 设有两个子句C和D 若有置换 或代换 使得C D成立 便说子句C把子句D归类 或说D被C归类 于是子句D可以从S中删除 删除策略 其中 C 表示子句C在代换 下的例式 即将子句C中的变元用 中的项代换所得的结果 例如C p x D p a Q a 取 a x 于是有C p a 于是有 p a p a Q a 其中逗号代表的是析取 删除策略 设子句序列C1 C2 Ck是从S推出Ck的演绎 若在演绎的过程中随时删除永真公式和被前面归类的子句 就称在这个演绎的过程中实行了删除策略 删除策略是完备的 即对于不可满足的子句集合S来说 如果在水平浸透法中使用删除策略 那麽一定存在一个空子句 Sn 删除策略 下面给出归类算法 SubsumptionAlgorithm 设D L1 L2 Lm 有 a1 x1 a2 x2 an xn 其中x1 x2 xn是D中所有变元的符号 a1 a2 an是C和D中都没有的互不相同的常量符号 步1令W L1 Lm K 0 U0 C 步2若 Uk则算法停 C归类D 步3令Uk 1 R C1 C2 C1 Uk C2 W 步4若Uk 1 则算法停 C不归类D 步5令K K 1 转步2 删除策略 由于U0 U1 Uk 序列中 后一个子句集中的每一个子句一定比前一个子句集中的亲本子句少一个文字 而子句中的文字是有限的 所以 最后一定存在一个n使Uk 或 Un即算法是可停的 本算法是完备的 即子句C归类子句D 当且仅当归类算法停在步2 删除策略 例如给定C P x Q f x a D P h y Q f h y a P z 试判定C是否可归类D 解 令 b y c z W P h b Q f h b a P c K 0U0 P x Q f x a K 0 因 U0 删除策略 U1 Q f h b a P h b Q f c a 因U1 K K 1 K 1 因 U1 求U2 因U2 K K 1 K 2 U2算法停 C归类D D可以被删除 删除策略 例设C P x x D P f x y P y f x 试判定C是否归类D 解 令 a x b y W P f a b P b f a K 0U0 P x x K 0 因 U0 求U1 因U1 算法停 C不归类D 线性输入策略 线性归结是这样一种归结 首先从子句集合S中选取一个称作顶子句的子句C0开始作归结 其次是归结过程中所得到的归结式Ci立即同另一子句Bi进行归结得归结式Ci 1而Bi属于S或是已出现过的归结式Cj j i 线性输入策略 例S P Q P Q P Q P Q 选取顶子句C0 P Q线性归结过程1 P Q2 P Q3 P Q4 P Q5 Q1和26 P5和37 Q6和48 7和5 线性输入策略 顶子句的选择直接影响着归结的效率 最好选得C0使S C0 是可满足的 线性输入策略具有简单和高效的优点 但它是不完备的 也就是说 即使子句集是不可满足的 用线性归结时也不一定能归结出空子句 例如对子句集S P x Q x P y Q y P u Q u P t Q t 用线性输入策略却归结不出空子句 单文字子句策略 如果一个子句只包含一个文字 则称它为单文字子句 单文字子句策略要求参加归结的两个子句中必须有一个子句是单文字子句 例如 设有子句集 I x R x I a R y L y L a 其中 I x R x 是目标公式经否定后得到的子句 用单文字子句策略归结过程如下 单文字子句策略构 1 I x R x 2 I a SS1 3 R y L y 4 L a 5 R a 1 和 2 及代换 a x 6 R a 3 和 4 及代换 a y S2 7 I a 1 和 6 及代换 a x 8 L a 3 和 5 及代换 a y S3 9 NIL 单文字子句策略 单文字子句策略归结的效率显然是很高的 但是它不是完备的 因为如果没有单文字子句则不能使用单文字子句策略 祖先过滤策略 当两个子句进行归结时只要满足下列两个条件 1 C1与C2中至少有一个是初始子句集中的子句 2 如果两个子句都不是初始子句集中的子句 则一个应是另一个的祖先 所谓一个子句 例如C1 是另一个子句 例如C2 的祖先是指C2是由C1与别的子句归结后得到的归结式 祖先过滤策略 祖先过滤发是完备的 例设有子句集S P x Q x P y Q y P u Q u P t Q t 祖先过滤策略 用祖先过滤法求解过程如下 P x Q x P y Q y S3 P u Q u P t Q t P x 1和 及代换 x y Q x 3和 及代换 x u P t 4和 及代换 x t NIL5和 及空代换 与 或形演绎推理 针对归结演绎中存在的问题 人们提出了多种非子句集定理证明的方法 其中尼尔逊提出的与 或形的演绎推理就是其中的一种 它不再把有关知识转化成子句形 而是把领域知识及已知事实分别用蕴含式及与 或形表示出来 然后通过运用蕴含式进行演绎推理 从而证明某个目标公式 与 或形演绎推理 与 或形的演绎推理分为正向演绎 逆向演绎和双向演绎 分别介绍如下 与 或形正向演绎推理它从某个已知事实出发 正向地使用蕴含式 规则 进行演绎推理 直到目标公式的某个终止条件为止 推理过程中需要对已知的事实 规则及目标公式的表示形式变化成要求的形式 与 或形正向演绎推理 事实表达式的与 或形变换及其树形表示事实表达式的与 或形表示和化子句的过程类似 只是最后不必化成子句的合取形式 也不必消去合取词 与 或形正向演绎推理 例如对下述事实表达式化成与 或形 x y Q y x R y P y S x y 解上式 y Q y a R y P y S a y 消去存在量词 Q z a R y P y S a y 消去全称量词 使主要合取式中的变元不重名 与 或形正向演绎推理 事实表达式的与 或树表示 Q z a R y P y S a y Q z a R y P y S a y R