第3章 谓词逻辑与归结原理.ppt

人工智能 第三章谓词逻辑与归结原理 1 概述 本章的内容与目标智能体如何认识事物并且进行推理用形式化的语言描述推理过程机器证明的一般方法 归结原理 2 概述 语言自然语言 人们在日常生活中所使用的语言文字半形式化语言 自然语言加特定的符号 如数学语言 定义 定理等 形式化语言 用精确的数学或机器可处理的公式定义的语言 逻辑学语言 弗雷格Frege 1879 p q p r p r p 3 怪物洞穴 人工智能的经典实验环境 怪物洞穴 wumpus世界 洞穴有多个房间组成某个房间中藏着一只怪物wumpus 它会吃掉进入这个房间的人 相邻房间中能够感觉到臭味某些房间中有陷阱 进入房间会被陷阱吞噬 相邻房间中能够感觉到微风游戏的主角是一个智能体 可以进入相邻的房间 对角线不可以 智能体有且仅有一支箭 用这支箭可以射杀怪物某个房间中有金子 游戏的目标是智能体找到金子 4 怪物洞穴 智能体行动的关键是要根据获得的信息推理 从而判断哪个房间有怪物 哪个房间有陷阱 哪个房间是安全的 房间 4 2 和 2 3 有陷阱 房间 3 4 有怪物 房间 4 3 有金子 5 3 1命题逻辑 6 3 1命题逻辑 命题 能够判断真假的陈述句陈述句真值唯一 可用二进制表示用小写字母进行标识例1 北京是中国的首都 2 华南师范大学位于岗顶附近 3 1 1 24 计算机系的学生必修C或JAVA 5 坐着花生过黄河5 x 1 26 吃饭了吗 7 南无阿弥陀佛8 我正在说假话 7 3 1命题逻辑 简单命题与复合命题简单命题 原子命题 一个命题无法分解为更简单的子命题复合命题 由简单命题用联结词联结而成的命题1 由若干简单命题组成 2 由联结词联结例 1 北京是中国的首都 2 华南师范大学位于岗顶附近 3 计算机系的学生必修C或JAVA 4 这家的报价单配置合理并且价格低廉 5 李四是犯罪嫌疑人 李四有犯罪动机 8 3 1命题逻辑 合式公式 单个常量或者变量的命题构成合式公式联结词联结的合式公式的组合也是合式公式合式公式的有限次组合称为命题公式命题公式 有限次合式公式组合的形式化描述 本书中以大写字母标识 9 3 1命题逻辑 基本联结 连接 符号 非 否定 与 合取 AND的首字母 或 析取 vel 蕴含式A a b表示 如果a 则b 等价联结符号的优先级 10 3 1命题逻辑 将命题从语言表述转换为命题公式step1 找出简单命题 并用符号表示step2 分析简单命题间的逻辑关系 用联结符号进行描述例 1 3不是偶数令 p表示 3是偶数 p 2 教室里有30名男生和10名女生令 p表示 教室里有30名男生 q表示 教室里有10名女生 p q 3 如果天下雨 出门带伞令p表示 天下雨 q表示 出门带伞 p q 4 只要不下雨 我就骑自行车上班令p表示 天下雨 q表示 骑自行车上班 p q 5 只有不下雨 我才骑自行车上班令p表示 天下雨 q表示 骑自行车上班 q p 11 3 1命题逻辑 例 怪物洞穴如果房间 1 1 中有臭味 则房间 1 2 或 2 1 中有怪物表示房间 i j 中有臭味表示房间 i j 中有怪物 练习 如果房间 1 1 中没有臭味 则房间 1 2 和 2 1 中没有怪物 12 3 1命题逻辑 练习 扫雷游戏设Xi j表示方格 i j 中有一个地雷 写出方格 1 1 周围恰好有2颗地雷的命题公式 12345 54321 13 3 1命题逻辑 命题公式的赋值对命题公式中的所有的命题变量各赋给一个值0 1 真值表 14 3 1命题逻辑 复合命题的真值例 p 周杰伦是一个流行歌手q 人工智能是计算机科学的一个分支r 牛在天上飞求下列复合命题的真值 p q p q p q p q r q r p r p r p r p r 我们关心的是复合命题中命题之间的真值关系 而不关心命题的内容 15 3 1命题逻辑 命题公式的分类重言式或永真式tautology 设A为任一命题公式 若A在它的各种赋值下取值均为真 则称A是重言式例 P P矛盾式或永假式contradictory设A为任一命题公式 若A在它的各种赋值下取值均为假 则称A是永假式 例 P P 16 3 1命题逻辑 可满足式satisfiable设A为任一命题公式 如果存在一组取值使A为真 则A为可满足式 即 对于命题公式A 若A不是矛盾式 则称A是可满足式 例 P Q非重言式的可满足式既是可满足式 又不是重言式 17 3 1命题逻辑 等值逻辑运算逻辑等值 等号连接的命题公式等价 基本等值算式P80交换律 A BB A A BB A 结合律 A B CA B C A B CA B C 分配律 A B C A B A C A B C A B A C 双重否定律 AA 等幂律 AA A AA A 摩根律 A B A B A B A B 18 3 1命题逻辑 吸收律 A A B A A A B A 同一律 A 0A A 1A 零律 A 11 A 00 排中律 A A1矛盾律 A A0 蕴含等值式 A B A B 等价等值式 A B A B B A 假言易位式 A B B A 等价否定等值式 A B A B 归谬论 A B A B A 19 3 1命题逻辑 合取范式与析取范式简单析取式 有限个命题变元或其否定 析取联结符p q p q p q合取范式 有限个简单析取式 合取p p q p q 简单合取式 有限个命题变元或其否定 合取p q p q p q析取范式 有限个简单合取式 析取p p q p q 20 3 1命题逻辑 任意命题公式都存在等值的析取范式和合取范式求取合取范式的步骤1 利用蕴含等值式和等价等值式消去命题公式中除 以外的联结词2 利用摩根律 双重否定律等进行置换 将 移到括号里面3 利用分配律得到合取范式 21 3 1命题逻辑 例P82计算 p q r s的合取范式 p q r s 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 分配律 22 3 1命题逻辑 例P82计算 p q r p的合取范式 p q r p p q r p 蕴含等值式 p q r p 蕴含等值式 p q r p 摩根律 p q r p 双重否定律 p q p r p 分配律 p q r p 等幂律 23 3 1命题逻辑 课堂练习计算合取范式 p q q p p q q p 24 3 1命题逻辑 命题逻辑推理逻辑结论 如果A B为重言式 则称B是A的逻辑结论 记作A B 常用推理定律 附加 A A B 简化 A B A假言推理 A B A B拒取式 A B B A析取三段论 A B A B假言三段论 A B B C A C 等价三段论 AB BC AC 构造型二难 A B C D A C B D 25 3 1命题逻辑 命题逻辑推理规则前提引入规则任何证明的步骤上 都可以引入前提 结论引入规则任何证明的步骤上 所得到的结论都可以作为后续证明的前提 置换规则任何证明的步骤上 命题公式中任何子命题都可以用与之等值的命题公式置换 26 3 1命题逻辑 例 P84如果今天下雨 则要带雨伞或雨衣 如果走路上班 则不带雨衣 今天下雨 走路上班 证明要带伞 解 p 今天下雨 q 带雨伞 r 带雨衣 s 走路上班前提 p q r s r p s求证 q证明 1 p q r p前提引入 2 p q r p q r假言推理 3 s r s前提引入 4 s r s r假言推理 5 q r r q析取三段论 27 3 1命题逻辑 例怪物洞穴表示房间 i j 中有臭味表示房间 i j 中有怪物表示房间 i j 中有微风表示房间 i j 中有陷阱 28 3 1命题逻辑 初始状态 在房间 1 1 处没有感觉到微风 也没有臭味 则相邻房间为安全的 既没有怪物也没有陷阱 前提 结论 证明 前提引入等价等值式简化前提引入拒取式摩根律 29 3 1命题逻辑 归结原理证明的一般方法由已知条件正向推导结论 演绎推理假定结论不成立 逆向推导与已知条件矛盾 反证法命题逻辑证明的归谬思想P85归结原理的思想 如果证明A B为永假式 则得证 30 31 3 1命题逻辑 归结方法的思想1 将待证明问题转化为其逆命题例 条件A 求证B 即A B其逆命题为 A B2 求合取范式 得到子句集构成合取范式的有限个简单析取式构成的集合就是子句集3 对子句集进行归结 得到空子句 32 3 1命题逻辑 将待证明问题转化为另一种形式证明问题的一般形式 已知 A成立求证 B成立即 证明A BA B A B蕴含等值式 A B 摩根律A B如果退出矛盾 则结论成立 33 3 1命题逻辑 例 证明G是F的逻辑结论F1 P WF2 WG P分析 已知条件为 P W W 结论为 P则 变换形式为 P W W P 34 3 1命题逻辑 子句与子句集P86对问题的变换形式 求其合取范式对于一个合取范式 该范式中的每一条简单析取式都是一个子句 子句集 合取范式下的所有子句构成其子句集 例 p p q p q 子句集为 p p q p q 35 3 1命题逻辑 归结方法如果p q与 q r都为真 则p r为真证明1真值表 证明2前提 p q q r 结论 p r证明 p q q r p q q r 蕴含等值式与双重否定律 p r 假言三段论p r蕴含等值式 36 3 1命题逻辑 归结式例 p q p q 归结后为 q 归结的目标 空子句对于一个合取范式 如果有一个子句不可满足 则子句集就不可满足 该合取范式为永假式若一个子句集中包含空子句 则这个子句集一定是不可满足的例 p p 归结后为 37 3 1命题逻辑 归结法步骤建立待归结命题公式 将证明A B为真转化为证明A B为矛盾式求合取范式 得到子句集对子句集进行归结归结式作为新子句加入子句集进行归结当归结式为空子句 时停止 证明结束 出现空子句 表示该子句集不可满足归结法的完备性 如果A B成立 则利用归结法一定可以得到证明 38 3 1命题逻辑 例 证明 p q q p 证明 要证明原命题为真 只需证明 p q q p 为恒假 p q q p p q q p 蕴含等值式 p q q p摩根律于是 子句集为 1 p q2 q3p p q q p 4 p1 2归结5 3 4归结由此可得 p q q p 为恒假 原命题为真 p p p q q p p p q q 39 3 1命题逻辑 例 怪兽洞穴1 在房间 1 1 处没有感觉到微风 也没有臭味 2 在房间 1 2 处感觉到微风 但没有感觉到臭味 3 在房间 2 1 处没有感觉到微风 但感觉到臭味 求证 房间 3 1 处有怪物 房间 1 3 处有洞穴 房间 2 2 是安全的 40 3 1命题逻辑 前提 求证 证明 要证明原命题为真 只需证明以下命题为恒假 41 3 1命题逻辑 于是 得到子句集为 42 3 1命题逻辑 1 s1 22 w1 13s2 14 s2 1 w1 1 w2 2 w3 15s1 2 w1 16s1 2 w2 27 w3 1 8w1 1 w2 2 w3 13 4归结9w2 2 w3 18 2归结10w2 29 7归结11s1 210 6归结12 11 1归结 43 3 1命题逻辑 思考 归结算法的计算机实现 S0 S1 S2 S3 终止条件 1 生成了空子句 证明结束2 循环结束 没有可以添加的新语句 待证明的定理不成立 44 3 1命题逻辑 好的归结控制策略初始状态优先选择包含结论的子句进行归结 之后每次都选择上一次归结得到的归结式与其他子句归结容易犯的错误字句集1 P Q2 P Q3 1 2归结 3 Q Q1 2归结 不允许同时归结两个项 45 3 1命题逻辑 归结方法是一种机械化的 可在计算机上加以实现的推理方法归结方法是一种反向推理形式提供了一种自动定理证明的方法归结的半完备性当定理可以证明时 归结方法是完备的当定理不可证明时 归结方法得不到任何结论 算法不一定会停止 46 3 2谓词逻辑 47 3 2 1基本概念 命题逻辑描述简单的陈述性命题 但表示量化和谓词过于繁琐 也难以表示个体间的关系 例 现在课堂上的所有学生都在上人工智能课命题逻辑s1 张三在上人工智能课s2 李四在上人工智能课s3 王五在上人工智能课 例2 用命题逻辑归结原理证明 人都是妈生的 张飞是人 所以张飞是妈生的 p 人都是妈生的q 张飞是人r 张飞是妈生的 p q rp q r 48 3 2 1基本概念 谓词逻辑Class x 表示x在上人工智能课x 张三 就得到了s1 x 李四 就得到了s2 x 王五 就得到了s3 Class x y 表示x在上y课x 张三 y 人工智能 表示张三在上人工智能课x 李四 y 线性代数 表示李四在上线性代数课x 王五 y 睡觉 表示王五在上睡觉课 49 3 2 1基本概念 命题是一个陈述句 它一般可分成主语和谓语两部分 有时还需要用到量词 主语 指独立存在的客体 可以是具体事物或抽象概念 也称为个体谓词 描述个体词性质或个体之间关系的词个体域 表示个体变量的取值范围 常用D表示常量 表示具体性质或关系的个体或者谓词变量 表示抽象或泛指的个体或者谓词 量词 表示数量的词 任意量词 表示 任意 所有 也称为全称量词存在量词 表示 存在 50 3 2 1基本概念 例 关羽是人 张飞是人 这是两个不同的命题 其主语 个体 不同但是谓词是相同的 是人 把谓语部分抽出来 假设Human x 表示x是人这两个命题都可以用这个谓词来描述Human guanyu Human zhangfei 其中x属于个体变量 guanyu和zhangfei属于个体常量 51 3 2 1基本概念 例 1 所有的人都是要死的2 有的人能够活到100岁P x 表示x是要死的 Q x 表示x活到100岁个体域D为人类集合个体域D为总个体域集合引入特殊谓词R x 表示x是人 52 3 2 1基本概念 语言描述转换为谓词公式1 确定并说明谓词2 确定个体和个体域3 确定量词4 判断谓词间的逻辑关系 53 3 2 1基本概念 例 我是计算机系的学生1 确定并说明谓词 方法一 Student x y 表示X是Y系的学生2 个体域 X 学生的集合 y 系的集合Student I computer 方法二 Computer x 表示X是计算机系的学生Computer I 注意 必须对谓词进行说明P I computer 54 3 2 1基本概念 1 定义并说明谓词Unlike x y 表示x不喜欢y课2 个体域x学生的集合 y课程的集合3 量词存在 例 有学生不喜欢上人工智能课 Like x y 表示x喜欢y课 Student x 表示x是学生Like x y 表示x喜欢y课 个体域x 人的集合 逻辑关系 与 55 3 2 1基本概念 例 任何人的兄弟都是男性确定并说明谓词Brother x y 表示x是y的兄弟Male x 表示x是男性个体域Brother x y x y 人的集合Male x x 人的集合量词任意确定逻辑关系与 或 非 蕴含 等价 56 3 2 1基本概念 例 不管黑猫白猫 抓住老鼠就是好猫定义并说明谓词Cat x y 表示是x是y颜色的猫Goodcat x 表示x是好猫Catch x Mouse 表示x能抓住老鼠个体域x 猫的集合 y 颜色的集合谓词间的关系Cat x y 与Catch x Mouse 蕴含Goodcat x 量词 任意 57 3 2 1基本概念 量词使用中的注意事项不同的个体域中 命题符号化的形式可能不同没有给定个体域的情况下 应考虑全总个体域如果个体域为有限集 对任意谓词P x 有 多个量词同时出现时 不能颠倒其先后顺利 否则会改变公式的含义 58 3 2 1基本概念 例 love x y 表示x喜爱y表示对任意的x 都存在喜爱的对象y 即 每一个人都会喜爱某人 表示存在都一个y 任意的人x都喜爱他 即 上帝 OR 大众 59 3 2 2一阶谓词逻辑 原子公式 设是任意n元谓词 是项 则称为原子公式 项 任何常量是项 任何变量是项 n 1个参数的任何表达式 其中 是项 而f是n阶的函数 是项 闭包条款 其他东西都不是项 60 3 2 2一阶谓词逻辑 谓词公式原子公式是谓词公式 若A为谓词公式 则 A也是一个谓词公式 若A和B都是谓词公式 则 A B A B A B 和 AB 也都是谓词公式 若A是谓词公式 和也都是谓词公式 只有有限次应用上述规则得到的公式 才是谓词公式 61 3 2 2一阶谓词逻辑 对于 x称为指导变量A称为相应量词的辖域 x p x x在辖域A中的出现称为约束出现x以外的变量在辖域A中的出现称为自由出现 x p x y 62 对于 指导变量 的辖域 x y都是约束出现 3 2 2一阶谓词逻辑 例对于 指导变量 的辖域 x y是约束出现还是自由出现y是约束出现 x是自由出现 63 3 2 2一阶谓词逻辑 不同量词如果采用相同的指导变量名 易引起混淆一般要求不同的量词使用不同的指导变量名称 64 3 2 2一阶谓词逻辑 当在一个公式中 一个变量符号既是约束出现的变量 又是自由出现的变量时 需要作变量符号更换 换名规则 将量词辖域中某个约束出现的变量及其指导变量替换为此辖域中未出现过的个体变量符号x既作为指导变量约束出现又自由出现 因此要换掉其中之一换名规则更换的是指导变量可替换为 65 3 2 2一阶谓词逻辑 替代规则 对某自由出现的个体变量用与原公式中未出现过的变量符号去替代 且处处替代 x既作为指导变量约束出现又自由出现 且多处自由出现替代规则更换的是自由出现的变量 且处处替代替换为 66 3 2 2一阶谓词逻辑 谓词公式的解释对谓词公式中的各种变量制定具体的常量去替代一个解释包括非空个体域DD中一部分特定元素 D上一些特定的函数 D上一些特定的谓词 如果谓词公式在特定解释下为真 称这个解释满足这个谓词公式 是这个谓词公式的一个模型永真与不可满足 67 3 2 2一阶谓词逻辑 例 P92给定解释I如下个体域 函数f x f 2 3 f 3 2谓词 P x 为P 2 0 P 3 1Q x y 为Q i j 1 i j 2 3R x y 为R 2 2 R 3 3 1 R 2 3 R 3 2 0求解释I下 下列谓词公式的真值1 2 68 3 2 2一阶谓词逻辑 解1 P f 2 Q 2 f 2 P f 3 Q 3 f 3 P Q 2 P Q 3 1 1 0 1 12 R 2 2 R 2 3 R 3 2 R 3 3 1 0 0 1 1 69 3 2 3谓词演算与推理 谓词演算公式约束变量换名规则 Q为任意量词 Qx P x Qy P y Qx P x z Qy P y z 量词消去等值式 对于有穷个体域量词否定等值式量词分配等值式 70 3 2 3谓词演算与推理 量词辖域收缩与扩张等值式 71 3 2 3谓词演算与推理 前束范式 约束在前面的范式将所有的量词都移到最左边就得到了前束范式与合取范式类似 所有的谓词公式都可以改写成前束范式的形式求前束范式的步骤前束范式中每个量词的指导变量不同 如果指导变量相同 则需要利用换名规则进行替换 如果自由变量与指导变量相同 则需利用换名规则或替代规则替换其中之一利用量词辖域收缩扩张等值式替换 72 3 2 3谓词演算与推理 例P94求前束范式量词与指导变量 自由出现的变量 换名规则替代规则P933 7 73 3 2 3谓词演算与推理 P933 8P933 3P933 4 74 3 2 3谓词演算与推理 谓词推理例 20世纪70年代的漫画都是日本漫画家创作的 这幅漫画是20世纪70年代的作品 因此它是日本漫画家的作品解 设P x 属于20世纪70年代的漫画Q y 属于日本漫画家的作品a 一幅漫画前提 结论 Q a 证明 前提引入量词消去前提引入假言推理 75 3 2 4谓词知识表示 谓词逻辑表达的规范形式P是谓词 而表示个体 主体或者客体 知识库 表达知识的一组谓词公式的集合 语句的集合对环境 规则等信息的结构化描述基于知识的智能体的核心构件 76 3 2 4谓词知识表示 定义谓词例1 小李与小张打网球Play x y z 表示x y在进行z运动Play Li Zhang tennis 2 我在华南师范大学当教师Work x y z 表示x在y单位从事z工作Work Me Scnu teacher 3 怪物洞穴中某个房间有微风 有臭味 没有怪物 没有陷阱 没有金子Roomi j x y z m n 参数分别对应有没有微风 臭味 怪物 陷阱 金子Roomi j 1 1 0 0 0 77 78 3 2 4谓词知识表示 谓词比命题更加细致地刻画知识 表达能力强如 北京是个城市 City x 把城市这个概念分割出来 把 城市 与 北京 两个概念连接在一起 而且说明 北京 是 城市 的子概念 有层 谓词可以代表变化的情况如 City 北京 真 City 煤球 假在不同的知识之间建立联系 79 3 2 4谓词知识表示 在不同的知识之间建立联系如 Human x Lawed x 人人都受法律管制 x是同一个人 Commit x Punished x x不一定是人也可以是动物 而 Human x Lawed x commit x Punished x 意为如果由于某个x是人而受法律管制 则这个人犯了罪就一定要受到惩罚 80 3 2 4谓词知识表示 谓词逻辑法是应用最广的方法之一 其原因是 谓词逻辑与数据库 特别是关系数据库就有密切的关系 在关系数据库中 逻辑代数表达式是谓词表达式之一 因此 如果采用谓词逻辑作为系统的理论背景 则可将数据库系统扩展改造成知识库 一阶谓词逻辑具有完备的逻辑推理算法 如果对逻辑的某些外延扩展后 则可把大部分的知识表达成一阶谓词逻辑的形式 知识易表达 81 3 2 4谓词知识表示 谓词逻辑法是应用最广的方法之一 其原因是 谓词逻辑本身具有比较扎实的数学基础 知识的表达方式决定了系统的主要结构 因此 对知识表达方式的严密科学性要求就比较容易得到满足 这样对形式理论的扩展导致了整个系统框架的发展 逻辑推理是公理集合中演绎而得出结论的过程 由于逻辑及形式系统具有的重要性质 可以保证知识库中新旧知识在逻辑上的一致性 或通过相应的一套处理过程检验 和所演绎出来的结论的正确性 而其它的表示方法在这点上还不能与其相比 82 3 2 4谓词知识表示 用逻辑 谓词 表示知识实质上是把人类关于世界的认识变成一个包含个体 函数和谓词的概念化形式 基本步骤 给出有关世界的个体 函数和谓词构造一阶谓词公式 集 对公式 集 给出解释 使该解释是相应公式 集 的一个模型 83 3 2 4谓词知识表示 为此逻辑表示法在实际人工智能系统上得到应用 3 2 4谓词知识表示 例 准前女友双眼皮 大眼睛doublefold x bigeyes x 一头乌黑的头发blackhair x thickhair x 一身漂亮的呢子大衣beautifuldress x 走路的姿态赛过模特graceful x 84 85 3 2 4谓词知识表示 例 一个房间里 有一机器人Robot 一个积木块Box 两个桌子A和B 怎样用逻辑法描述从初始状态到目标状态的机器人操作过程 先引入谓词 Table A 表示A是桌子EmptyHanded Robot 机器人Robot双手空空At Robot A 表示机器人Robot在A旁Holds Robot Box 机器人Robot拿着BoxOn Box A 积木块Box在A上 86 3 2 4谓词知识表示 设定初始状态 EmptyHanded Robot On Box A Table A Table B 目标状态是 EmptyHanded Robot On Box B Table A Table B 87 例 续 机器人的每个操作的结果所引起的状态变化 可用对原状态的增添表和删除表来表示 如机器人有初始状态是把Box从A桌移到B桌上 然后仍回到Alcove 这时同初始状态相比有 增添表On Box B 删除表On Box A 又如机器人从初始状态 走近A桌 然后拿起Box 这时同初始状态相比有 增添表At Robot A Holds Robot Box 删除表At Robot Alcove EmptyHanded Robot On Box A 88 例 续 进一步说 机器人的每一操作还需要先决条件 如机器人拿起A桌上的Box这一操作 先决条件 On Box A Box在A上 At Robot A 机器人在A旁边 EmptyHanded robot 机器人手空空 89 例 续 先决条件成立与否的验证可以使用归结法 如将初始状态视作已知条件 而将要验证的先决条件作为结论 便可使用归结法了 归结过程如下 1 At Robot A 2 EmptyHanded Robot 3 On Box A 4 Table A 5 Table B 6 On Box A At Robot A EmptyHanded Robot 先决条件之否定 7 At Robot A EmptyHanded Robot 3 68 EmptyHanded Robot 1 79 NULL2 8于是验证了先决条件的成立 90 3 2 4谓词知识表示 存在问题 谓词表示越细 推力越慢 效率越低 但表示清楚 实际中是要折衷的 3 3谓词逻辑归结原理 91 3 3 1归结原理 命题逻辑归结原理 将由前提A得到结论B的证明过程转化为证明A B为矛盾式将其转化为合取范式 得到子句集对于形如的公式求取子句集时 可以分别求各自的子句集 再取并集利用归结原理消去互补项 直到得到空子句 92 3 3 1归结原理 例 P Q R P Q P R 转化为待归结命题公式 P Q R P Q P R 求子句集 分别对 P Q R 和 P Q P R 两部分求取子句集 再取并集 1 P Q R P Q R P Q R 2 P Q P R P Q P R P Q P R P Q P R P Q P R 子句集为 P Q R P Q P R 93 3 3 1归结原理 归结 1 P Q R2 P Q3 P4 R5 P R1 2归结6 R3 5归结7 4 6归结因此得证 94 子句集为 P Q R P Q P R 3 3 1归结原理 95 3 3 1归结原理 谓词逻辑归结原理的重点如何对前束合取范式消去量词命题逻辑谓词逻辑如何利用置换与合一对不同变量的子句进行置换命题逻辑谓词逻辑 96 3 3 1归结原理 求前束合取范式 方法一 先转化为前束范式 再将辖域中的谓词公式转化为合取范式方法二 1 消去联结词 和 2 将联结词 向内深入 使之只作用于原子公式 3 利用换名或替代规则使所有约束变元的符号都不同 并且自由变元与约束变元的符号也不同 4 利用量词辖域的扩张和收缩 扩大量词至整个公式 5 再将辖域中的谓词公式转化为合取范式 97 3 2 3谓词演算与推理 量词辖域收缩与扩张等值式 98 3 2 3谓词演算与推理 求前束合取范式 x P x Q x x P x Q x x P x Q x x P x Q y x P x Q y x P x Q y 1 消去 和 2 向内深入 3 换名或替代 4 量词前束 5 辖域中的公式化为合取范式 99 3 3 2Skolem标准型 例求前束合取范式 100 3 3 2Skolem标准型 Skolem标准型 对前束合取范式消去所有的量词 P100第一步 消去存在量词 1 如果 之前 左边 没有任意量词 则用常量替换 的指导变量可用常量b替换x消去存在量词 得P b a 2 如果 之前 左边 有任意量词 则用任意量词的函数替换 的指导变量可用f x 替换y消去存在量词 第二步消去任意量词 简单的省略即可 101 3 3 2Skolem标准型 例 1 消去存在量词 y和 u y前面有任意量词 指导变量为x 因此用f x 替换y u前面有任意量词 指导变量为x 因此用g x 替换u2 消去任意量词 102 3 3 2Skolem标准型 例判断下列的消去量词的过程是否正确 证明 x yG x y yG x y 消去 x G x a 消去 y对任意x 都存在一个恒定常量a 使G x a 成立 x yG x y xG x f x 消去 y G x f x 消去 x对任意x 都存在一个与之对应的f x 使G x f x 成立 103 3 3 3子句集 定义文字 不含任何联结词的谓词公式子句 一些文字或其非的析取子句集 所有子句的集合计算过程将谓词公式转化为前束合取范式消去存在量词 略去任意量词 得Skolem标准型将各子句提出 得到子句集谓词公式不可满足 当且仅当其子句集不可满足的形如的谓词公式在求子句集时可以分别对求子句 再取其并集 104 3 3 1归结原理 谓词逻辑归结原理的重点如何对前束合取范式消去量词命题逻辑谓词逻辑如何利用置换与合一对不同变量的子句进行置换命题逻辑谓词逻辑 105 3 3 4置换与合一 置换 形如的有限集合xi必须是变量 称为置换变量ti可以是常量 变量或者函数 称为置换项表示用项ti替换谓词公式中的变量xi要求ti xi xi不能循环的出现在另一个ti中 x y y z x y y x x y y z z x 106 3 3 4置换与合一 例 设有公式P x f y b 置换1为 s1 z x w y P x f y b s1 P z f w b 置换2为 s2 a y P x f y b s2 P x f a b 置换3为 s3 q z x a y P x f y b s3 P q z f a b 置换4为 s4 c x a y P x f y b s4 P c f a b 置换5为 s5 x b 107 3 3 4置换与合一 例 设 f y x z y a x b y y z 对L P x f y b 先做 置换 再做 置换 即求 108 3 3 4置换与合一 置换的合成 对谓词公式L 设 t1 x1 t2 x2 tn xn 和 u1 y1 u2 y2 un yn 为两个置换 则 称为 和 的合成 可由下式得到1 如果 则消去2 当 删去 109 3 3 4置换与合一 例 设 f y x z y a x b y y z 求 1 如果ti xi 则消去ti xi 2 当 删去 110 3 3 4置换与合一 例 对子句集 P x P a 做置换 a x 得到 P a P a P x y P a b Q x 做置换 a x b y P a b P a b Q 111 3 3 4置换与合一 合一 设有公式集 如果存在一个置换 使 则称 是F的一个合一 如果谓词公式F1 F2可合一 那么就是一对互补项 P x P a 经合一 a x 得到 P a P a 谓词逻辑归结原理 如果子句集中的两个字句含有互补项 则可以进行归结消去 112 3 3 4置换与合一 例 下列字句都可以归结 P x P x P x P a 经合一 a x 后 P x P a 可合一 P x y P a z 经合一 a x z y P x y P a z 可合一这些子句的文字可合一 都可以进行归结 P a x f g y P z f a f u 需要一个判断公式集能否合一的算法 113 3 3 4置换与合一 最一般合一 mgu 设是谓词公式F的一个合一 如果对于F的任意一个合一 都存在一个置换 使 则称是一个最一般合一 求取办法 对每一项逐一比较并进行合一置换P1041 令2 令3 如果已经合一 停止迭代 否则 找不一致集4 若中存在元素和 且不出现于中 转5 否则 不可合一5 令 6 k k 1 转3 114 3 3 4置换与合一 例 P a x f g y P z f a f u 计算mgu解 1W P a x f g y P z f a f u 23W0未合一 从左到右找不一致集 45令 6k k 1 转3 115 3 3 4置换与合一 3 W1未合一 从左到右找不一致集 4 5 令 6 k k 1 转33 W2未合一 从左到右找不一致集 4 5 令已合一 116 3 3 5归结式 归结式 设为两个无公共变量的子句 分别是的文字 如果可合一 则为的归结式例 1P x Q x y 与 P a R b z 的归结式 经合一 a x 置换归结得到 2P x y Q x R x 与 P a z Q b 的归结式 经合一 a x z y 归结得到 经合一 b x 归结得到 P b y R b P a z 117 3 3 5归结式 几种不能归结的情况谓词不一致不能进行归结如 P x 与 Q x 不能归结常量之间不能进行归结如 P a 与 P b 不能归结 不能在常量之间置换 a b 变量与其函数之间不能进行归结如 P x 与 P f x 不能归结 不能做置换 f x x 不能同时消去两个互补对 118 3 3 5归结式 如果子句可以简化 应该先简化再归结例C1可以简化 做合一置换 f x y 取mgu g a x 归结式为Q b Q g g a 119 3 3 6归结过程 写出谓词关系公式写出待归结的谓词表达式化为Skolem标准型求子句集S对S中的互补子句进行归结归结式仍加入S 反复进行归结得到空子句 得证 120 3 3 6归结过程 例 人都是妈生的 张飞是人 张飞是妈生的定义谓词 Mum x 表示x是妈生的Human x 表示x是人前提 x Human x Mum x Human ZF 结论 Mum ZF 写出否命题 121 3 3 6归结过程 1 Human x Mum x 2 Human ZF 3 Mum ZF 3与1归结 经置换 得到4 Human ZF 5 4与2归结得到 所以 否命题为恒假 原命题为真 优先选包含结论的子句归结 ZF x 122 3 3 6归结过程 例 已知 R1 会朗读的生物是识字的 R2 海豚不识字 R3 海豚是很机灵的 证明 有些很机灵的东西不会朗读 分析 1 需要几个谓词 2 海豚是否必须设为谓词 3 生物是否必须设为谓词 R x 表示x会朗读W x 表示x识字D x 表示x是海豚C x 表示x是机灵的个体域 生物 123 3 3 6归结过程 结论 换名 124 3 3 6归结过程 4 5归结 a t 6 1归结 a x 7 2归结 a y 8 3归结 125 3 3 6归结过程 例 设任何通过计算机考试并获奖的人都是快乐的 任何肯学习或幸运的人都能通过所有的考试 张不肯学习但他是幸运的 任何幸运的人都能获奖 求证 张是快乐的定义谓词 Pass x y 表示x通过y考试Win x prize 表示x能获奖Lucky x 表示x是幸运的Study x 表示x肯学习Happy x 表示x是快乐的 126 3 3 6归结过程 写出谓词公式 前提 结论 Happy zhang 取否 Happy zhang 证明 对前提和结论分别求子句 127 3 3 6归结过程 得到两个子句 128 3 3 6归结过程 得子句 Study zhang Lucky zhang 得子句 Luck w Win w prize 结论 Happy zhang 共得到7条子句 129 3 3 6归结过程 1 2 3 4 Study zhang 5 Lucky zhang 6 Luck w Win w prize 7 Happy zhang 8 zhang x 1 79 zhang w 8 610 9 511 zhang u computer v 10 312 11与5归结 得 结论 130 3 3 7归结过程控制策略 控制的要点要解决的问题是归结方法的知识爆炸控制的目的是归结点尽可能少控制的原则是删除不必要的子句或对参加归结的子句加以限制仅选择合适的子句进行归结 避免多余的 不必要的子句归结式出现 131 3 3 7归结过程控制策略 删除策略1 删除永真子句2 删除可被其他子句归类的子句归类 如果两个子句C和D 若有置换 使 则称子句C把D归类 可从子句集中删除D例 两个子句C P x D P a Q y 还原为谓词公式 P x P a Q y 取置换 a x 可知子句C把D归类 D可删除 132 3 3 7归结过程控制策略 支撑集策略一个不可满足的子句集S的子集T 如果S T是可满足的 则T为S的支撑集对于A B定理证明问题来说 B就是支撑集归结过程中每次都选择支撑集及其归结式与其他子句归结 133 134 例 S P Q P R Q R R 取T R 支持集归结过程 1 P Q 2 P R 3 Q R 4 R 5 P 2 4 6 Q 3 4 7 Q 1 5 8 P 1 6 9 R 3 7 10 6 7 3 3 7归结过程控制策略 语义归结策略将子句集按一定的语义分为两部分每部分内的子句不允许进行归结 同时引入文字次序 归结时 其中一个子句的被归结文字是该子句中排序最前的文字 例 S P Q R P Q Q R R 文字次序为P Q R 令解释I P Q R 在I下为假的子句记为s1 为真的语句记为s2 则 135 3 3 7归结过程控制策略 归结如下 1s22s13s14s251 2归结 s26R5 3归结 s17 6 4归结 136 3 3 7归结过程控制策略 线性归结策略每次都用上一次归结得到的归结式与其他子句归结 137 138 139 例 S P Q P Q P Q P Q 选取顶子句C0 P Q 线性归结过程 1 P Q 2 P Q 3 P Q 4 P Q 5 Q 1 2 6 P 5 3 7 Q 6 4 8 7 5 顶子句的选择直接影响着归结的效率 如可选得C0使S C0 是可满足的 3 3 7归结过程控制策略 单元归结策略每次归结都有一个子句是单元子句 即只含一个文字的子句 140 141 例 S P Q P R Q R R 单元归结过程 1 P Q 2 P R 3 Q R 4 R 5 P 4 2 6 Q 4 3 7 Q 5 1 8 P 6 1 9 R 7 3 10 7 6 3 3 7归结过程控制策略 输入归结策略每次归结必有一个子句是原始子句集中的子句 142 143 例 S P Q P R Q R R 单元归结过程 1 P Q 2 P R 3 Q R 4 R 5 P 4 2 6 Q 4 3 7 Q 5 1 8 P 6 1 9 R 7 3 10 7 6 144 Herbrand定理 问题 一阶逻辑公式的永真性 永假性 的判定是否能在有限步内完成 145 Herbrand定理 1936年图灵 Turing 和邱吉 Church 互相独立地证明了 没有一般的方法使得在有限步内判定一阶逻辑的公式是否是永真 或永假 但是如果公式本身是永真 或永假 的 那么就能在有限步内判定它是永真 或永假 对于非永真 或永假 的公式就不一定能在有限步内得到结论 判定的过程将可能是不停止的 146 Herbrand定理 Herbrand的思想定义 公式G永真 对于G的所有解释 G都为真 思想 寻找一个已给的公式是真的解释 然而 如果所给定的公式的确是永假的 就没有这样的解释存在 并且算法在有限步内停止 147 Herbrand定理 H域H解释语义树结论 Herbrand定理 148 Herbrand定理 H域H解释语义树结论 Herbrand定理 149 Herbrand定理 H域 基本方法 因为量词是任意的 所讨论的个体变量域D是任意的 所以解释的个数是无限 不可数的 简化讨论域 建立一个比较简单 特殊的域 使得只要在这个论域上 该公式是不可满足的 此域称为H域 150 Herbrand定理 H域 设G是已给的公式 定义在论域D上 令H0是G中所出现的常量的集合 若G中没有常量出现 就任取常量a D 而规定H0 a Hi Hi 1 所有形如f t1 tn 的元素 其中f t1 tn 是出现于G中的任一函数符号 而t1 tn是Hi 1的元素 i 1 2 规定H 为G的H域 或说是相应的子句集S的H域 不难看出 H域是直接依赖于G的最多只有可数个元素 151 152 H域例题 例1 S P a P x P f x 依定义有H0 a H1 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 153 H域例题 例2 S P z P x Q y 依定义有H0 a a是论域D中一常量 H1 H0H2 H1 H a 154 H域例题 例3 S P f x a g y b 依定义有H0 a b H1 a b f a g a f b 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 H H0 H1 H2 如果在S中出现函数形如f x a 仍视为f x1 x2 的形式 这时若H0 a b 则H1中除有f a a f b a 外 还出现f a b f b b 155 H域例题 例4 设子句集S P x Q y f z b R a 求H域解 H0 a b 为子句集中出现的常量H1 a b f a b f a a f b a f b b 156 H域例题 H2 a b f a b f a a f b a f b b f a f a b f a f a a f a f b a f a f b b f b f a b f b f a a f b f b a f b f b b f f a b f a b f f a b f a a f f a b f b a f f a b f b b f f a a f a b f f a a f a a f f a a f b a f f a a f b b f f b a f a b f f b a f a a f f b a f b a f f b a f b b f f b b f a b f f b b f a a f f b b f b a f f b b f b b H H1 H2 H3 157 Herbrand定理 H域 几个基本概念f tn f为子句集S中的所有函数变量 t1 t2 tn为S的H域的元素 通过它们来讨论永真性 原子集A 谓词套上H域的元素组成的集合 如A 所有形如P t1 t2 tn 的元素 即把H中的东西填到S的谓词里去 S中的谓词是有限的 H是可数的 因此 A也是可数的 158 原子集例题 上例题的原子集为 A P a Q a a R a P b Q b a Q b b Q a b R b P f a b Q f a b f a b R f a b P f a a P f b a P f b b 一旦原子集内真值确定好 规定好 则S在H上的真值可确定 成为可数问题 159 Herbrand定理 H域H解释语义树结论 Herbrand定理 160 Herbrand定理 H域H解释语义树结论 Herbrand定理 161 Herbrand定理 H解释 解释I 谓词公式