第三章-王士同版

2020 4 8 1 第三章谓词逻辑与归结原理 华北电力大学计算机系刘丽 2020 4 8 2 第三章谓词逻辑与归结原理 归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略 2020 4 8 3 2020 4 8 4 第三章谓词逻辑与归结原理 归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略 2020 4 8 5 概述 推理技术 确定知识表达方法 将知识表示出来并存储到计算机中 利用知识来解决实际问题利用知识进行推理是知识利用的基础 是问题求解的主要手段如专家系统 智能机器人 模式识别 自然语言理解等推理按照某种策略从已有事实和知识推出结论的过程 推理是由程序实现的 称为推理机医疗诊断专家系统知识库中存储经验及医学常识数据库中存放病人的症状 化验结果等初始事实利用知识库中的知识及一定的控制策略 为病人诊治疾病 开出医疗处方就是推理过程 2020 4 8 6 概述 推理的分类演绎推理 归纳推理 默认推理确定性推理 不精确推理单调推理 非单调推理启发式推理 非启发式推理 2020 4 8 7 概述 从推出新判断的途径分演绎 归纳和默认推理演绎推理从全称判断推出特称判断或单称判断的过程 即从一般到个别的推理演绎推理中最常用的形式是三段论法 大前提和小前提 及结论 例如 所有的推理系统都是智能系统 一般的知识专家系统是推理系统 个体的判断所以 专家系统是智能系统 新判断没有增加新的知识 2020 4 8 8 概述 演绎推理 归纳推理和默认推理 归纳推理从足够多的事例中归纳出一般性结论的推理过程 是一种从个别到一般的推理过程常用的归纳推理有简单枚举法和类比法枚举法归纳推理是由已观察到的事物都有某属性 而没有观察到相反的事例 从而推出某类事物都有某属性 推理过程为 S1是PS2是P Sn是P S1 S2 Sn是S类中的个别事物 在枚举中兼容 S都是P 2020 4 8 9 概述 演绎推理 归纳推理和默认推理 归纳推理之枚举法枚举法归纳推理分完全归纳推理与不完全归纳推理完全归纳推理在进行归纳时考察了相应事物的全部对象 并根据这些对象是否都具有某种属性 从而推出这个事物是否具有这个属性完全归纳推理是必然性推理不完全归纳推理只考察了相应事物的部分对象 就得出了结论不完全推理得出的结论不具有必然性 属于非必然性推理 2020 4 8 10 概述 演绎推理 归纳推理和默认推理 归纳推理之类比法在两个或两类事物在许多属性上都相同的基础上 推出它们在其它属性上也相同 这就是类比法归纳推理类比法归纳可形式化地表示为 A具有属性a b c d eB具有属性a b c d B也具有属性e类比法的可靠程度决定于两个或两类事物的相同属性与推出的那个属性之间的相关程度 相关程度越高 则类比法的可靠性就越高归纳推理增加了知识 在机器学习部分称为归纳学习 2020 4 8 11 概述 演绎推理 归纳推理和默认推理 默认推理又称为缺省推理 是在知识不完全的情况下假设某些条件已经具备所进行的推理如 在条件A已成立的情况下 如果没有足够的证据能证明条件B不成立 则就默认B是成立的 并在此默认的前提下进行推理 推导出某个结论知识不完全的情况下也能进行推理如果到某一时刻发现原先所作的默认不正确 则要撤消所作的默认以及由此默认推出的所有结论 重新按新情况进行推理 2020 4 8 12 概述 按推理时所用的知识的确定性分确定性推理推理中所用的知识都是精确的归结反演 基于规则的演绎系统等都是确定性推理不精确推理基于不确定的推理规则进行 形成的结论也是不确定的专家系统中主要使用的是不精确推理 2020 4 8 13 概述 按推出的结论是否单调增加 或推出的结论是否越来越接近最终目标分 单调推理在推理过程中随着推理的向前推进及新知识的加入 推出的结论呈单调增加的趋势 并且越来越接近最终目标非单调推理在推理过程中随着推理的向前推进及新知识的加入 不仅没有加强已推出的结论 反而要否定它 使得推理退回到前面的某一步 重新开始一般非单调推理是在知识不完全的情况下进行的 2020 4 8 14 概述 按推理中是否运用与问题有关的启发性知识分启发式推理推理过程中 运用与问题有关的启发性知识 以加快推理过程 提高搜索效率A AO 等算法就属于此类推理非启发式推理推理过程中 不运用启发性知识 只按照一般的控制逻辑进行推理这种方法缺乏对求解问题的针对性 所以推理效率较低 容易出现 组合爆炸 问题 如宽度优先搜索法 2020 4 8 15 概述 推理的控制策略主要是指推理方向的选择 推理时所用的搜索策略及冲突解决策略等一般推理的控制策略与知识表达方法有关推理方向推理方向用于确定推理的驱动方式根据推理方向的不同 可将推理分为正向推理 反向推理和正反向混合推理无论按哪种方式进行推理 一般都要求系统具有一个存放知识的知识库 KB 一个存放初始事实和中间结果的数据库 DB 和一个用于推理的推理机 2020 4 8 16 概述 推理的控制策略 推理方向正向推理 事实驱动推理 是由已知事实出发向结论方向的推理 2020 4 8 17 概述 推理的控制策略 推理方向反向推理 以某个假设目标作为出发点的一种推理 又称为目标驱动推理或逆向推理 2020 4 8 18 概述 推理的控制策略 推理方向正反混合推理 2020 4 8 19 概述 推理的控制策略 搜索策略推理时 要反复用到知识库中的规则 而知识库中的规则又很多 这样就存在着如何在知识库中寻找可用规则的问题为有效控制规则的选取 可以采用各种搜索策略常用搜索策略 状态空间搜索 宽度优先搜索 深度优先搜索 有界深度优先搜索等 启发式搜索等 第三章 2020 4 8 20 概述 推理的控制策略 冲突解决策略推理过程中 系统要不断地用数据库中的事实与知识库中的规则进行匹配 当有一个以上规则的条件部分和当前数据库相匹配时 就需要有一种策略来决定首先使用哪一条规则 这就是冲突解决策略冲突解决策略实际上就是确定规则的启用顺序 2020 4 8 21 概述 推理的控制策略 推理的控制策略冲突解决策略 1 专一性排序如果某一规则的条件部分规定的情况比另一规则的条件部分所规定的情况更专门 则这条规则具有较高的优先级例 有如下规则 规则1 IFAANDBANDCTHENE 规则2 IFAANDBANDCANDDTHENF 数据库中A B C D均为真 这时规则1和规则2都与数据库相匹配 但因为规则2的条件部分包括了更多的限制 所以具有较高的优先级本策略是优先使用针对性较强的产生式规则 2020 4 8 22 概述 推理的控制策略 推理的控制策略3 冲突解决策略 2 规则排序规则编排的顺序就表示了启用的优先级 3 数据排序数据排序就是把规则条件部分的所有条件排序 按优先级次序编排 发生冲突时 首先使用在条件部分包含较高优先级数据的规则 4 就近排序把最近使用的规则放在最优先的位置 如果某一规则经常使用 则倾向于更多地使用这条规则 5 上下文限制上下文限制就是把产生式规则按它们所描述的上下文分组 在某种上下文条件下 只能从与其相对应的那组规则中选择可应用的规则 2020 4 8 23 概述 推理的控制策略 推理的控制策略3 冲突解决策略 6 按匹配度排序在不精确匹配中 为了确定两个知识模式是否可以进行匹配 需要计算这两个模式的相似程度 当其相似度达到某个预先规定的值时 就认为它们是可匹配的 若有几条规则均可匹配成功 则可根据它们的匹配度来决定哪一个产生式规则可优先被应用 7 按条件个数排序如果有多条产生式规则生成的结论相同 则要求条件少的产生式规则被优先应用 因为要求条件少的规则匹配时花费的时间较少不同的系统 可使用上述这些策略的不同组合 2020 4 8 24 概述 归结原理由J A Robinson于1965年提出定理证明的实质要对给出的 已知的 前提和结论 证明此前提推导出该结论这一事实是永恒的真理非常困难的 几乎是不可实现的要证明在一个论域上一个事件是永真的 就要证明在该域中的每一个点上该事实都成立论域是不可数时 该问题不可能解决即使可数 如果该轮域是无限的 问题也无法简单地解决 2020 4 8 25 概述 理论基础 Herbrand采用反证法的思想 将永真性的证明问题转化成为不可满足性的证明问题实现方法 Robinson的归结原理使得自动定理证明得以实现归结推理方法是机器定理证明的主要方法 2020 4 8 26 归结法的特点 归结法是一阶逻辑中 至今为止的最有效的半可判定的算法 也是最适合计算机进行推理的逻辑演算方法半可判定一阶逻辑中任意恒真公式 使用归结原理 总可以在有限步内给以判定 证明其为永真式 当不知道该公式是否为恒真时 使用归结原理不能得到任何结论 2020 4 8 27 归结法基本原理 采用反证法 反演推理方法 将待证明的表达式 定理 转换成为逻辑公式 谓词公式 然后再进行归结归结能够顺利完成 则证明原公式 定理 是正确的 2020 4 8 28 归结法基本原理 例 例 由命题逻辑描述的命题 A1 A2 A3和B 要求证明 如果A1 A2 A3成立 则B成立 即 A1 A2 A3 B是重言式 永真式 归结法的思路A1 A2 A3 B是重言式等价于A1 A2 A3 B是矛盾式 也就是永假式反证法 证明A1 A2 A3 B是矛盾式 永假式 2020 4 8 29 第三章谓词逻辑与归结原理 概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理 2020 4 8 30 第三章谓词逻辑与归结原理 概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理 2020 4 8 31 命题 描述事实 事物的状态 关系等性质的文字串 取值为真或假 表示是否成立 的句子称作命题命题 非真即假的简单陈述句能判断真假陈述句命题用小写字母p q r s等表示 2020 4 8 32 命题例 命题 能判断真假 不是既真又假 的陈述句简单陈述句描述事实 事物的状态 关系等性质例如 1 1 1 22 雪是黑色的 3 北京是中国的首都 4 到冥王星去渡假 判断一个句子是否是命题 有先要看它是否是陈述句 而后看它的真值是否唯一 以上4个例子都是命题 例如 1 快点走吧 2 到哪儿去 3 x y 10都不是命题 2020 4 8 33 命题表示公式 1 将陈述句转化成命题公式 如 设 下雨 为p 骑车上班 为q 1 只要不下雨 我骑自行车上班 p是q的充分条件 因而 可得命题公式 p q2 只有不下雨 我才骑自行车上班 p是q的必要条件 因而 可得命题公式 q p 2020 4 8 34 命题表示公式 2 例如 1 如果我进城我就去看你 除非我很累 设 p 我进城 q 去看你 r 我很累 则有命题公式 r p q 2 应届高中生 得过数学或物理竞赛的一等奖 保送上北京大学 设 p 应届高中生 q 保送上北京大学上学 r 是得过数学一等奖 t 是得过物理一等奖 则有命题公式公式 p r t q 2020 4 8 35 命题逻辑基础 数理逻辑的基本定义 命题逻辑基础 定义 合取式 p与q 记做p q析取式 p或q 记做p q蕴含式 如果p则q 记做p q等价式 p当且仅当q 记做pq 归结法的基础 2020 4 8 36 命题逻辑基础 数理逻辑的基本定义 定义 若A无成假赋值 则称A为重言式或永真式若A无成真赋值 则称A为矛盾式或永假式若A至少有一个成真赋值 则称A为可满足的析取范式 仅由有限个简单合取式组成的析取式合取范式 仅由有限个简单析取式组成的合取式 2020 4 8 37 命题逻辑基础 基本等值式 1 基本等值式24个交换率 p qq p p qq p结合率 p q rp q r p q rp q r 分配率 p q r p q p r p q r p q p r 2020 4 8 38 命题逻辑基础 基本等值式 2 摩根率 p q p q p q p q吸收率 p p q p p p q p同一律 p 0p p 1p蕴含等值式 p q p q假言易位式 p q p q 2020 4 8 39 命题逻辑基础 基本等值式 3 双重否定律p p零率律p 0p p 1p 书P80 2020 4 8 40 命题逻辑基础 合取范式 范式 公式的标准形式合取范式 单元子句 单元子句的或 的与 如 P P Q P Q 求合取范式的步骤求合取范式的基本原则利用 对 的分配律例 求取P Q R S的合取范式 1 消去对于 来说冗余的连接词2 内移或消去否定号3 利用分配律 2020 4 8 41 命题逻辑基础 合取范式 解 P Q R S P Q R S P Q R S P Q R S P Q R S P S Q R P S Q P S R 注意 将原有的命题公式整理 转换成为各个 或 语句的 与 否则后续推导没有意义转换基于数理逻辑的基本等值公式 或 转换到 与 中 2020 4 8 42 命题逻辑的推理规则 逻辑结论 有效结论 A B如A B为重言式 永真式 则称A推结论B的推理正确 B是A的逻辑结论称A B为由前件A推结论B的推理的形式结构可采用真值表法 等值演算法等证明逻辑结论逻辑结论也称为假言推理或演绎推理重言式表示为A B 2020 4 8 43 命题逻辑的推理规则 常用的推理定律 附加 A A B 简化 A B A假言推理 A B A B拒取式 A B B A析取三段论 A B A B假言三段论 A B B C A C等价三段论 A B B C A C构造性二难 A B C D A C B D 2020 4 8 44 命题逻辑的推理规则 常用的推理规则 前提引入规则 在证明的任何步骤上 都可以引入前提结论引入规则 在证明的任何步骤上 所证明的结论都可以作为后续证明的前提置换规则 在证明的任何步骤上 命题公式中的任何子命题都可以用与之等值的命题公式置换例如 可以用 p q置换p q 2020 4 8 45 命题逻辑的演绎推理 例1 例3 3 构造下列推理的证明 前提p q p r s t s r t结论q证明 s t前提引入 t前提引入 s 拒取规则 A B B A s r前提引入 r 假言推理 A B B C A C p r前提引入 p 拒取规则 p q前提引入 q 析取三段论 A B A B 2020 4 8 46 命题逻辑的演绎推理 例2 例3 4写出对应下面推理的证明 如果今天是下雨天 则要带雨伞或带雨衣 如果走路上班 则不带雨衣 今天下雨 走路上班 所以带伞 解 p 今天下雨 q 带伞 r 带雨衣 s 走路上班 前提 p q r s r p s结论 q证明 p q r 前提引入 p前提引入 q r 假言推理 s r前提引入 s前提引入 r 假言推理 q 析取三段论 2020 4 8 47 命题逻辑的归结 演绎推理 从一系列前提得出结论上两个例子归结方法 新推理方法理论基础是Herbrand定理将待证逻辑公式的结论 通过等值公式转换成附加前提 再证明该逻辑公式不可满足A1 A2 A3 B是重言式证明A1 A2 A3 B不可满足建立在子句集基础上 2020 4 8 48 命题逻辑基础 子句集 命题公式的子句集S合取范式形式下的子命题 元素 的集合是合取范式中各个合取分量的集合生成子句集的过程简单地理解为将命题公式合取范式中的与 置换为逗号 上例的合取范式 P S Q P S R 其子句集为S P S Q P S R 命题公式 P P Q P Q 其子句集S S P P Q P Q 2020 4 8 49 命题逻辑的归结 基本单元 简单命题 陈述句 例 命题 A1 A2 A3和B求证 A1 A2 A3成立 则B成立 即 A1 A2 A3 B反证法 证明A1 A2 A3 B是矛盾式 永假式 2020 4 8 50 命题逻辑的归结 合取范式和子句集 合取范式 命题 命题或的与 如 P P Q P Q 子句集S 合取范式形式下的子命题 元素 的集合例 命题公式 P P Q P Q 子句集S S P P Q P Q 2020 4 8 51 命题逻辑的归结法 归结式 归结式 归结法的核心设C1和C2是子句集中的任意两个子句 如果C1中的文字L1与C2中的文字L2互补 那么可从C1和C2中分别消去L1和L2 并将C1和C2中余下的部分按析取关系构成一个新子句C12 则称这一个过程为归结 称C12为C1和C2的归结式 称C1和C2为C12的亲本子句消去互补文字 用析取连接剩余部分例如 有子句 C1 P C1 C2 P C2 存在互补对P和 P 则可得归结式 C12 C1 C2 2020 4 8 52 命题逻辑的归结法 归结式性质 归结式性质 归结式C12是亲本子句C1和C2的逻辑结论C1 C2 C12任一使C1 C2为真的解释I下必有归结式C12为真注意 C1 C2 C12 反之不一定成立 C1 P C1 C2 P C2 C12 C1 C2 因为存在一个使C1 C2 为真的解释I 不妨设C1 为真 C2 为假 若P为真 则 P C2 就为假了 因此反之不一定成立 2020 4 8 53 命题逻辑的归结法 归结过程 建立待归结命题公式 根据反证法将所求证的问题转化成为命题公式 求证其是矛盾式 永假式 求取合取范式建立子句集归结对子句集中的子句使用归结规则归结式作为新子句加入子句集参加归结归结式为空子句 为止 说明子句集不可满足 即定理成立 归结完毕谓词归结 除有量词和函数以外 其余和命题归结一样 2020 4 8 54 命题逻辑归结例题 1 例题 证明公式 P Q Q P 证明 1 根据归结原理 将待证明公式转化成待归结命题公式 P Q Q P 2 分别将公式前项化为合取范式 P Q P Q结论求 后的后项化为合取范式 Q P Q P Q P两项合并后化为合取范式 P Q Q P 3 则子句集为 P Q Q P 2020 4 8 55 命题逻辑归结例题 2 子句集为 P Q Q P 4 对子句集中的子句进行归结可得 1 P Q2 Q3 P4 Q 1 3归结 5 2 4归结 由上可得原公式成立 2020 4 8 56 第三章谓词逻辑与归结原理 概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理 2020 4 8 57 第三章谓词逻辑与归结原理 概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理 2020 4 8 58 谓词逻辑归结基础 基本概念 一阶逻辑逻辑的基本定义基本概念个体词 表示主语的词个体常量 具体的或特定的个体个体变量 抽象的或泛指的个体谓词 刻画个体性质或个体之间关系的词谓词常量 具体性质或关系的谓词谓词变量 抽象或泛指的谓词量词 表示数量的词量词符号 全称 存在量词 2020 4 8 59 谓词逻辑归结基础 基本概念 例 小王是个工程师 8是个自然数 我去买花 小丽和小华是朋友 个体词 小王 工程师 我 花 8 小丽 小华 谓词 是个工程师 是个自然数 去买 是朋友 都是谓词前两个谓词表示的是事物的性质第三个谓词 去买 表示的一个动作也表示了主 宾两个个体词的关系最后一个谓词 是朋友 表示两个个体词之间的关系 2020 4 8 60 谓词逻辑归结基础 基本概念 一阶逻辑逻辑 以谓词的形式来表示动作的主体 客体公式及其解释个体常量 a b c个体变量 x y z谓词常量 P Q R谓词变量 P x Q x y R x b 量词符号 xP x xP x 2020 4 8 61 谓词逻辑归结基础 基本概念 原子公式 设P x1 x2 xn 是任意n元谓词 t1 t2 tn是项 则P t1 t2 tn 为原子公式谓词公式 原子公式是谓词公式若A是谓词公式 则 A 也是谓词公式若A B是谓词公式 则 A B A B A B A B 也是谓词公式若A是谓词公式 则 xA xA也是谓词公式只有有限次的应用 构成的符号串才是谓词公式 2020 4 8 62 谓词逻辑归结基础 基本概念 指导变量 xA xA中的x为指导变量辖域 xA xA中的A成为相应量词的辖域约束出现 在辖域 A 中 x的所有出现称为约束出现自由出现 在辖域 A 中 不是约束出现的其他变量的出现 称为自由出现 2020 4 8 63 谓词逻辑归结基础 基本概念 例 例如 1 所有的人都是要死的 2 有的人活到一百岁以上 在个体域D为人类集合时 可符号化为 1 xP x 其中P x 表示x是要死的 2 xQ x 其中Q x 表示x活到一百岁以上 在个体域D是全总个体域时 引入特殊谓词R x 表示x是人 可符号化为 1 x R x P x 其中 R x 表示x是人 P x 表示x是要死的 2 x R x Q x 其中 R x 表示x是人 Q x 表示x活到一百岁以上 2020 4 8 64 谓词逻辑归结基础 谓词公式等值式 量词否定等值式 x M x y M y x M x y M y 量词分配等值式 x P x Q x x P x x Q x x P x Q x x P x x Q x 消去量词等值式 设个体域为有穷集合 a1 a2 an x P x P a1 P a2 P an x P x P a1 P a2 P an 2020 4 8 65 谓词逻辑归结基础 谓词公式等值式 量词辖域收缩与扩张等值式 x P x Q x P x Q x P x Q x P x Q x P x Q x P x Q x Q P x Q x P x x P x Q x P x Q x P x Q x P x Q x P x Q x P x Q x Q P x Q x P x 2020 4 8 66 Skolem标准型 前束范式 SKolem标准型是在前束范式的基础上进行变量映射的前束范式如果A中的一切量词都位于该公式的最左边 不含否定词 且这些量词的辖域都延伸到公式的末端 则公式A是一个前束范式 Q1x1 Q2x2 Qnxn M x1 x2 xn 量词提到公式最前端时存在约束变量换名问题 要严守约束变元的换名规则 Qx M x Qy M y Qx M x z Qy M y z 例题 Qi 量词 M 母式 2020 4 8 67 w P w x y z P x y z u R x y z u w P w x y z P x y z u R x y z u w x y z u P w P x y z R x y z u 2020 4 8 68 Skolem标准型 前束范式中消去所有量词后形成的谓词公式为Skolem标准型Skolem标准型必须满足合取范式的条件任何一个谓词公式都可以化成与之对应的Skolem标准型 但注意 Skolem标准型不唯一 2020 4 8 69 Skolem标准型 转化过程 将谓词公式G转换成为前束范式消去量词量词消去原则 消去存在量词 如果存在量词左边没有任何全称量词 则只将其改写成为常量 a b等 如果是左边有全称量词的存在量词 消去时该变量改写成为全称量词的函数 f x g y 等 略去全称量词 简单地省略掉该量词 2020 4 8 70 Skolem标准型 例 将下式化为Skolem标准型 x y P a x y x y Q y b R x 解 第一步 消去 号 得 x y P a x y x y Q y b R x 第二步 深入到量词内部 得 x y P a x y x y Q y b R x x y P a x y x y Q y b R x 第三步 任意量词左移 利用分配律 得到 x y P a x y y Q y b R x 第四步 变元易名 存在量词左移 直至所有的量词移到前面 得 x y P a x y y Q y b R x x y P a x y z Q z b R x x y z P a x y Q z b R x 由此得到前述范式 2020 4 8 71 Skolem标准型 例 上页 x y z P a x y Q z b R x 第五步 消去 略去 消去 y 因为它左边只有 x 所以使用x的函数f x 代替之 这样得到 x z P a x f x Q z b R x 消去 z 同理使用g x 代替之 这样得到 x P a x f x Q g x b R x 略去全称变量 原式的Skolem标准型为 P a x f x Q g x b R x 例2 x p x x Q x x p x Q x 2020 4 8 72 Skolem定理 SKOLEM标准型定义 消去量词后的前束范式Skolem定理 谓词逻辑的任意公式都可以化为与之等价的前束范式 但其前束范式不唯一注意 谓词公式G的SKOLEM标准型同G并不等值例如有谓词公式G x p x 其skolem标准型G P a 解释I 个体域DI 0 1 常数a 0 谓词P x 为P 0 F P 1 T 则在解释I下G T G F 2020 4 8 73 子句集 定义 子句与子句集文字 不含任何连接词的谓词公式子句 一些文字的析取 谓词的和 空子句 不含任何文字的子句 子句集 所有子句的集合对于任一个公式G 都可以通过Skolem标准型 标准化建立起一个子句集与之相对应 2020 4 8 74 子句集 求取步骤 子句集S的求取 通过Skolem标准型求取G 前束范式 消去量词生成Skolem标准型 将Skolem标准型中的子句提出 表示为集合形式 即以 取代 并表示为集合形式注意Skolem标准型必须满足合取范式的条件 2020 4 8 75 P119例4 1 x P x Q x y S x y Q x x P x B x 化成子句集 1 蕴含等值式 x P x Q x y S x y Q x x P x B x 2 否定内移 x P x Q x y S x y Q x x P x B x 3 全称量词对 的分配律 x P x Q x y S x y Q x P x B x 4 量词辖域的扩张等值 x y P x Q x S x y Q x P x B x 5 分配律 朝合取范式进行 x y P x S x y Q x Q x S x y Q x P x B x 6 利用吸收率p p q p p p q p x y P x S x y Q x Q x P x B x x y P x S x y P x Q x Q x P x B x x y P x S x y Q x P x B x 7 去掉量词 P x S x f x Q x P x B x 8 子句变量标准化后 最终的子句集为 P x S x f x Q y P w B w 2020 4 8 76 子句集与谓词公式的不可满足性 G是不可满足的S是不可满足的G与S不等价 但在不可满足的意义下是一致的定理3 1 若G是给定的公式 而S是相应的子句集 则G是不可满足的 当且仅当S是不可满足的 注意 G真不一定S真 而S真必有G真即 S G 2020 4 8 77 子句集与谓词公式的不可满足性 定理3 1的推广 谓词公式G G1 G2 G3 Gn G的子句集S的求取可以分解成几个部分单独处理 如果Gi的子句集为Si 则有 S S1 S2 S3 Sn G的子句集不为S 但可以证明 SG与S 在不可满足的意义上是一致的 SG不可满足 S1 S2 S3 Sn不可满足 2020 4 8 78 求取子句集例 1 例 对所有的x y z来说 如果y是x的父亲 z又是y的父亲 则z是x的祖父 又知每个人都有父亲 试问对某个人来说谁是它的祖父 求 用一阶逻辑表示这个问题 并建立子句集 解 这里我们首先引入谓词 P x y 表示x是y的父亲Q x y 表示x是y的祖父ANS x 表示问题的解答 2020 4 8 79 求取子句集例 2 对第一个条件 如果x是y的父亲 y又是z的父亲 则x是z的祖父 一阶逻辑表达式如下 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 对结论 某个人是他的祖父B x y Q x y 否定后得到子句 x y Q x y ANS x S B Q x y ANS x 则得到的相应的子句集为 SA1 SA2 S B 2020 4 8 80 第三章谓词逻辑与归结原理 概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理 2020 4 8 81 第三章谓词逻辑与归结原理 概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理 2020 4 8 82 归结原理 方法 和命题逻辑一样但由于有函数 所以要考虑合一和置换 2020 4 8 83 置换 置换 在一个谓词公式中用置换项去置换变量定义 置换是形如 t1 x1 t2 x2 tn xn 的有限集合 其中 x1 x2 xn是互不相同的变量 t1 t2 tn是不同于xi的项 常量 变量 函数 ti xi表示用ti置换xi 并且要求ti与xi不能相同 而且xi不能循环地出现在另一个ti中 例如 a x c y f b z 是一个置换 g y x f x y 不是一个置换 2020 4 8 84 置换 定义 设 是一个置换 E是一个表达式 把对E施行置换 即把E中出现的个体变元xi用ti替换 记为E 例 a x f b y c z G P x y z 求G G P a f b c 2020 4 8 85 置换的合成 设 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 i 1 2 n 当yi x1 x2 xn 时 删去uj yj j 1 2 m 最后剩下的元素所构成的集合合成即是对ti先做 置换然后再做 置换 置换xi 2020 4 8 86 置换的合成 例 设 f y x z y a x b y y z 求 与 的合成 解 先求出集合 f b y x y z y a x b y y z f b x y y a x b y y z 其中 f b x中的f b 是置换 作用于f y 的结果 y y中的y是置换 作用于z的结果 在该集合中 y y满足定义中的条件i 需要删除 a x b y满足定义中的条件ii 也需要删除 最后得 f b x y z 2020 4 8 87 合一 定义 设有公式集F F1 F2 Fn 若存在一个置换 可使F1 F2 Fn 则称 是F的一个合一 同时称F1 F2 Fn是可合一的合一可以简单地理解为 寻找相对变量的置换 使两个谓词公式一致 2020 4 8 88 合一 例子 例 设有公式集F P x y f y P a g x z 则 a x g a y f g a z 是它的一个合一注意 一般说来 一个公式集的合一不是唯一的 2020 4 8 89 最一般合一 定义 最一般合一设 是公式集F的一个合一 如果对F的任意一个合一 都存在一个置换 使得 则称 是一个最一般合一 MostGeneralUnifier 简记为mgu 一个公式集的最一般合一是唯一的 2020 4 8 90 最一般合一 mgu的求取方法对于给定谓词公式F1和F2 采用逐一比较找出不一致 并作出相应的合一置换 可求得mgu 2020 4 8 91 mgu求取方法 令w F1 F2 令k 0 w0 w 0 如果wk已合一 停止 k mgu 否则 找不一致集Dk若Dk中存在元素vk和tk 其中vk不出现于tk中 转5 否则 不可合一令 k 1 k tk vk wk 1 wk tk vk w k 1k k 1 转3若F1和F2可合一 算法必停止与3 2020 4 8 92 mgu的例子 例 W P a x f g y P z f a f u 其中F1 P a x f g y F2 P z f a f u 求F1和F2的最一般合一 2020 4 8 93 2020 4 8 94 2020 4 8 95 归结式 和命题逻辑一样消去互补对 但要考虑变量的合一与置换设C1 C2是两个无公共变量的子句 L1和L2分别是C1和C2的文字 如果L1 L2有最一般合一 则R C1 L1 C2 L2 称作子句C1 C2的一个二元归结式 而L1和L2为被归结的文字例子 2020 4 8 96 P x Q x y 与 P a R b z 的归结式Q a y R b z a x P x y Q x R x 与 P a z Q b 的归结式Q a R a Q b a x y z P b y R b P a z b x 2020 4 8 97 归结原理 归结的注意事项 谓词的一致性 P 与 Q 不可以常量的一致性 P a 与 P b 不可以 变量 P a 与 P x 可以变量与函数 P x x 与 P x f x 不可以 P x x 与 P x f y 可以 不能同时消去两个互补对 P Q与 P Q得空 不可以先进行内部简化 置换 合并 例子 2020 4 8 98 归结原理 归结的过程 归结的过程写出谓词关系公式 用反演法写出谓词表达式 SKOLEM标准型 子句集S 对S中可归结的子句做归结 归结式仍放入S中 反复归结过程 得到空子句 得证 2020 4 8 99 例题 快乐学生 问题 假设任何通过计算机考试并获奖的人都是快乐的 任何肯学习或幸运的人都可以通过所有的考试 张不肯学习但他是幸运的 任何幸运的人都能获奖 求证 张是快乐的 证明 先将问题用谓词表示如下 R1 任何通过计算机考试并获奖的人都是快乐的 x Pass x computer Win x prize Happy x R2 任何肯学习或幸运的人都可以通过所有考试 x y Study x Lucky x Pass x y R3 张不肯学习但他是幸运的 Study zhang Lucky zhang R4 任何幸运的人都能获奖 x Luck x Win x prize 结论 张是快乐的 的否定 Happy zhang 2020 4 8 100 例题 快乐学生 问题 由R1及逻辑转换公式 P W H P W H 可得 1 Pass x computer Win x prize Happy x 由R2 2 Study y Pass y z 3 Lucky u Pass u v 由R3 4 Study zhang 5 Lucky zhang 由R4 6 Lucky w Win w prize 由结论 7 Happy zhang 结论的否定 8 Pass w computer Happy w Lucky w 1 6 w x 9 Pass zhang computer Lucky zhang 8 7 zhang w 10 Pass zhang computer 9 5 11 Lucky zhang 10 3 zhang u computer v 12 11 5 2020 4 8 101 例题 例4 4 已知前提为F x P x y Q y y R y S x y 求证结论G x R x x y P x y Q y 成立证明 先按前面所讲的方法将前提和结论化为子句集 前提F所对应的子句集为 P x y Q y R f x P x y Q y S x f x 结论G否定对应子句集为 R z P A B Q B 2020 4 8 102 例题 例 1 x是y的父亲 y是z的父亲 则x是z的祖父 2 老李是大李的父亲 3 大李是小李的父亲问 三人之中谁和谁是祖孙关系 2020 4 8 103 例题 某些患者喜欢所有医生 没有患者喜欢庸医 所以没有医生是庸医 2020 4 8 104 第三章谓词逻辑与归结原理 概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略 2020 4 8 105 第三章谓词逻辑与归结原理 概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略 2020 4 8 106 归结过程的控制策略 要解决的问题归结方法的知识爆炸控制策略的目的归结点尽量少控制策略的原则删除不必要的子句 或对参加归结的子句做限制 以使仅选择合适的子句对其归结避免多余的 不必要的归结式出现 2020 4 8 107 控制策略的方法 1 删除策略 名词解释 归类 设有两个子句C和D 若有置换 使得C D成立 则称子句C把子句D归类 例 P x 归类P a Q y a x Q y 归类P x Q y P x 归类P x P x 归类P a P a x P y b 归类P a b b x a y 2020 4 8 108 控制策略的方法 1 删除策略 由于小的可以代表大的 所以小的吃掉大的了若对S使用归结推理过程中 当归结式Cj是重言式 永真式 和Cj被S中子句和子句集的归结式Ci i j 所归类时 便将Cj删除这样的推理过程便称做使用了删除策略的归结过程 2020 4 8 109 控制策略的方法 1 删除策略 主要思想 归结过程在寻找可归结子句时 子句集中的子句越多 需要付出的代价就会越大如果在归结时能把子句集中无用的子句删除掉 就会缩小搜索范围 减少比较次数 从而提高归结效率 2020 4 8 110 控制策略的方法 1 删除策略 评价 对阻止不必要的归结式的产生来缩短归结过程是有效的在Cj产生后方能判别它是否可被删除 这部分计算量是要花费的 只是节省了被删除的子句又生成的归结式使用删除策略的归结 少做了归结但不影响产生空子句 即 删除策略的归结推理是完备的不是可以归结的谓词公式都可以用删除策略来处理删除策略 完备 2020 4 8 111 控制策略的方法 2 支撑集策略 支撑集 设有不可满足子句集S的子集T 如果S T是可满足的 则T是支持集支撑集策略从开始到得到 的整个归结过程中 只选取不同时属