人工智能逻辑表示及归结系统.ppt

第6章基于谓词逻辑的归结方法 一阶谓词逻辑概述归结原理归结反演系统基于归结法的问题求解 定义 逻辑学是研究人类思维活动规律的科学 方法 利用数学 符号化 公理化 形式化 的方法来研究这些规律 作用 是表达人类思维和推理的最精确和成功的方法 成为AI的重要基础 表现方式和人类自然语言非常接近便于计算机做精确处理分类 经典逻辑和非经典逻辑两大类 经典逻辑中命题逻辑和一阶谓词逻辑是基础 1一阶谓词逻辑概述 命题的定义 表示知识的陈述性形式或具有真假意义的陈述句 例 A 张平是学生 B 树叶是绿色的 命题的类型 原子命题 表达单一意义 不能再分解 如P 天在下雨 Q 天晴复合命题 由连接词 标点和原子命题构成 如 P Q可表示 如果天在下雨则天不晴 命题逻辑就是研究命题与命题之间关系的符号逻辑系统 包含语法 语义 演算等 1 1命题概念 原子命题是命题逻辑中最基本的单元 不能对其进行分解 也不能对其结构进行分析 引发的问题 限制了它的使用 为了突破这种束缚 发展了谓词逻辑 原子命题可分解 以命题中的谓词为基础进行分析研究 1 2谓词概念 原子命题分解为谓词 个体2部分 例 1 3是质数 x是质数 F x 2 王二生于武汉市 x生于y G x y 3 7 2 3 x y z H x y z 3 王二 武汉市 7等 称为个体 具体 代表个体的变元 称为个体变元 抽象 刻画个体性质或个体之间关系的词叫谓词 如 是质数 生于 谓词中包含的个体数目称为谓词的元数 在谓词P x1 x2 xn 中 若每个xi都是个体常量 变元或函数 则称它为一阶谓词 若某个xi本身又是一个一阶谓词 则称它为二阶谓词 谓词与命题的区别 更强的表达能力 1 有概括能力例如 是一个城市 谓词CITY X 2 可表示变化着的情况命题值是恒真或恒假 谓词值可因参数而异3 可在不同的知识之间建立高级联系HUMAN X X是人 LAWED X X受法律约束 COMMIT X X犯法 PUNISHED X X受法律制裁HUMAN X LAWED X 人人都要受法律约束COMMIT X PUNISHED X 犯罪 就要受惩罚 HUMAN X LAWED X COMMIT X PUNISHED X 2归结原理 定理证明 已知一公式集F1 F2 Fn 要证明一个公式W是否成立 即要证明W是公式集的逻辑推论 方法 直接法 F1 F2 Fn W是永真式 间接法 反证法 F1 F2 Fn W为永假基本思想 采用反证法将待证明的表达式转换为逻辑公式 然后再进行归结 归结能够顺利完成 则证明原定理是正确的 2 1归结原理概述 2 1归结原理概述 续 理论依据 空子句 一种没有任何解释能满足的子句 其取值总是假 简记为 或NIL 用归结法从子句集S导出的扩大子句集S1 S 归结式 其不可满足性是不变的 待证 技术思路 设法检验原 或扩充的 子句集S是否含有空子句 若S集中存在空子句 则表明S为不可满足的 过程 S S1 S2 Sn归结过程可以一直进行下去 也就是要通过归结过程演绎出S的不可满足性来 从而使定理得到证明 几个概念 不含有任何连接词的命题 谓词 公式称为原子公式 原子 原子或原子的否定统称为文字 子句是由一些文字组成的析取式 不包含任何文字的子句称为空子句 不能用任何解释所满足 子句构成的集合 称为子句集 2 2命题逻辑的归结法 1 归结式的定义及性质归结 设C1与C2是子句集中的任意两个子句 如果C1中的文字L1与C2中的文字L2互补 那么从C1和C2中分别消去L1和L2 并将两个子句中的余下部分析取 构成一个新的子句C 这一过程称为归结 C C1和C2的归结式 C1和C2 C的亲本子句 没有互补对的两子句没有归结式 例 设C1 P Q R C2 Q S C1中L1 Q与C2中L2 Q互补 得 C P R S 例 设C1 P C2 PP与 P互补 可得 C 例 设C1 P Q C2 Q R C3 P 首先对C1 C2进行归结 得C12 P R 再对C12 C3归结 得C123 R 定理 两个子句C1和C2的归结式C是C1和C2的逻辑结论 即C1 C2 C 证明 设C1 L C1 C2 L C2 通过归结可得到C C1 C2 因为C1 L C1 C1 L C1 L C2 L C2 L C2 C1 C2 C1 L L C2 由假言三段论得到 C1 L L C2 C1 C2 而 C1 C2 C1 C2 C C1 C2 C 证毕 推论 子句集合S C1 C2 Cn 与S1 C C1 C2 Cn 的不可满足性是等价的 C是C1和C2的归结式 即S1是对S应用归结后得到的 证明 设S是不可满足的 则C1 C2 Cn中必有一个为假 因而S1必为不可满足的 设S1是不可满足的 则对于不满足S1的任一解释I 可能有两种情况 I使C为真 则C1 C2 Cn中必有一子句为假 因而S是不可满足的 I使C为假 则根据定理有C1 C2为假 即I或使C1为假 或使C2为假 因而S也是不可满足的 由此 S和S1的不可满足性是等价的 同理可证Si和Si 1 Si导出的扩大的子句集 的不可满足性也是等价的 其中i 1 2 总结 归结原理就是从子句集S出发 应用归结推理规则导出子句集S1 再从S1出发导出S2 依次类推 直到某一个子句集Sn出现空子句为止 根据不可满足性等价原理 若已知Sn为不可满足的 则可逆向依次推得S必为不可满足的 用归结法证明定理 只涉及归结推理规则的应用问题 过程比较简单 因而便于实现机器证明 2 命题逻辑的归结过程 命题逻辑中 若给定公理集F和命题P 则归结证明过程可归纳为 把F转化为子句集表示 得子句集S0 把命题P的否定式 P也转化成子句集表示 并将其加到S0中 得S S0 P 对子句集S反复应用归结推理规则 直到导出含有空子句的扩大子句集为止 即出现归结式为空子句的情况时 表明已找到了矛盾 证明过程结束 例 设已知公理集为P 1 P Q R 2 S T Q 3 T 4 求证R 化成子句集表示后得S P P Q R S Q T Q T R 归结过程很简单 如右图的演绎树所示 由于根部出现了空子句 因此命题R得到证明 P Q R P Q Q T T T Q P R 2 3谓词逻辑中的归结原理 归结原理对子句集的基本要求 命题级 无量词约束子句只是文字的析取否定符只作用于单个文字子句间默认为合取在谓词逻辑中 由于表达式中包含有变元 所以需要考虑变量的约束问题 作用范围 1 谓词公式化子句集的方法 2 在应用归结法时 先对公式作变量置换和合一等处理 得到互补的基本式 然后才能进行归结 新问题1 量词问题 谓词演算中 一般有两种形式 前束范式和SKOLEM范式 前束范式 若一个谓词公式P的所有量词均非否定地出现在P的前部 且量词辖域是整个公式 称P为前束范式 如F Q1x1 Qnxn M Qi 2值 M 析取式 SKOLEM范式 消去前束范式中的所有量词 方法如下 后所得到的谓词公式 也称SKOLEM标准型 若变量不受全称量词的约束 左边无 可用任意常量代替该变量 否则 用以其为因变量的函数代替该存在量词 函数形式 几元函数 依赖于受几个全称量词约束 省略 1 谓词公式的标准化 化子句集的方法 xP x y P y P f x y y Q x y P y 1 消蕴涵符理论根据 a b a b xP x y P y P f x y y Q x y P y 2 移动否定符理论根据 a b a b a b a b x P x x P x x P x x P x 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 化子句集的方法 续1 3 变量标准化即 对于不同的量词约束 对应于不同的变量方法 x A x x B x x A x y B y x P x y P y P f x y w Q x w P w 4 量词左移 保序前移到M的前部 方法 x A x y B y x y A x B y x y w P x P y P f x y Q x w P w 化子句集的方法 续2 5 消存在量词 skolem化 原则 对于一个受存在量词约束的变量 如果它不受全程量词约束 则该变量用一个常量代替 如果它受全程量词约束 则该变量用一个函数代替 x y w P x P y P f x y Q x w P w y P a P y P f a y Q a g y P g y 化子句集的方法 续3 6 化为合取范式即 a b c d e f 的形式方法 P x Q x R x P x Q x P x R x P x Q x R x P x Q x R x P x Q x R x P x Q x R x P x Q x R x P x Q x R x y P a P y P f a y Q a g y P g y y P a P y P f a y P a Q a g y P a P g y 化子句集的方法 续4 7 隐去全程量词 P a P y P f a y P a Q a g y P a P g y 8 表示为子句集 以逗号替代所有的合取符号 P a P y P f a y P a Q a g y P a P g y 9 变量标准化 变量换名 即 不同的子句 使用不同的变量 P a P y1 P f a y1 P a Q a g y2 P a P g y3 课堂小练习 化下列公式成子句形式 1 x y P x y Q x y 2 x y P x y Q x y 3 x y P x y Q x y R x y 2 置换和合一 问题2 表达式是否相同或匹配 P x Q y 与P a R z 思路 个体变量的替换 方法 置换和合一置换 在谓词公式中用项 常 变 函数 替换变量 形如 s t1 v1 t2 v2 tn vn 对公式E实施置换s后得到的公式称为E的例 记作Es 例 s1 z x A y 则 P x f y B s P z f A B 2 置换和合一 续1 合成置换 有时需对表达式进行多次置换 如用s1 s2依次进行置换 即 Es1 s2 这时可以把两个置换合成为一个置换 记为s1s2 合成置换是由两部分组成的 一部分仍是s1的置换对 只是s1中的项被s2作了置换 另一部分是s2中与s1不同的那些变量对 例如 s1 g x y z s2 A x B y C w D z s1s2 g A B z A x B y C w 性质 Es1 s2 E s1s2 结合律 但一般情况下置换是不可交换的 即s1s2 s2s1 s2s1 A x B y C w D z s1s2 2 置换和合一 续2 合一就是通过项对变量的置换 而使表达式 文字 一致 若存在一个置换s使得表达式集 Ei 中每一个元素经置换后的例有 E1s E2s E3s 则称表达式集 Ei 是可合一的 这个置换s称作 Ei 的合一者 例 P x f y B P x f B B s A x B y 得 P A f B B 2 置换和合一 续3 如果g是公式集 Ei 的一个合一者 如果对 Ei 的任意一个合一者s都存在一个置换s 使得s gs 则称g为表达式 Ei 的最简单合一者mgu 例 P x f y B P x f B B g B y 为该式的mgu 因为 s A x B y 置换s A x 使s gs 求最简单合一者的算法 1 令W F1 F2 输入2 k 0 W0 W g0 循环次数 公式集合 置换的初始化3 如果Wk已合一 停止 gk mgu 成功退出否则 找不一致集Dk 4 若Dk中存在元素vk和tk 其中vk不出现于tk中 转 5 否则 不可合一 失败退出5 令gk 1 gk tk vk Wk 1 Wk tk vk 置换合成 公式集合变换6 k k 1转 3 2 置换和合一 续4 例 S P a x h g z P z h y h y 1 g0 Sg0不是单元素集 故求不一致集D0 a z 2 g1 g0 a z Sg1 P a x h g a P a h y h y 不是单元素集 故D1 x h y 3 g2 g1 h y x Sg2 Sg1 h y x P a h y h g a P a h y h y 不是单元素集 故D2 g a y 4 g3 g2 g a y Sg3 Sg2 g a y P a h g a h g a P a h g a h g a 是可合一的 即g3 a z h y x g a y a z h y x g a y a z h g a x g a y 是一个mgu 3 谓词逻辑中的归结式 归结式 对于子句C1 L1和C2 L2 如果L1与 L2可合一 且s是其合一者 则 C1 C2 s是其归结式 例 P x Q y P f z R z Q y R z s f z x 选不同文字对做归结时 可得不同的归结式练习 C1 P x f y Q y C2 P z f A Q z 3 谓词逻辑中的归结式 续 注意点 被归结的子句C1 C2应具有不同的变量 方法 变量换名在求归结式时 不能同时消去两个互补文字对 消去两个互补文字对所得到的结果不是亲本子句的逻辑推论 例 C1 P Q C2 P Q 如在参加归结的子句内含有可合一的文字 则应先对这些文字进行合一 化简后再归结 例 C1 P x P f a Q x C2 P y R b 定义谓词写出已知条件和结论的谓词关系公式化为Skolem标准型求子句集合S对S中可归结的子句做归结 置换和合一 归结式仍放入S中 反复归结过程看能否导出空子句 4 谓词逻辑中的归结过程 例 已知 1 会朗读的动物是识字的 2 海豚都是不识字的 3 有些海豚很机灵 证明 有些动物很机灵但不会朗读 已知 1 x R x L x 2 x D x L x 3 x D x I x 求证 x I x R x 化简前提条件公式 结论取反 得子句集 1 R x L x 2 D y L y 3a D A 3b I A 4 I z R z A z A x A y 1 R x L x 2 D y L y 3a D A 3b I A 4 I z R z 从子句集求归结式 并将它加进子句集 连续进行直到产生空子句为止 上图的归结过程代表一个可行的证明过程 归结反演树 3归结反演系统3 1产生式系统的基本算法 综合数据库 子句集 子句间为合取关系 规则集合 IFcx Si 和cy Si 有归结式rxyTHENSi 1 Si rxy 目标条件 Sn中出现空子句过程1Clauses S S为初始的基本子句集 2untilNIL是Clauses的元素 do 3begin4在Clauses中选两个不同的可归结的子句ci cj5求ci cj的归结式rij 6Clauses rij Clauses7end 3 2搜索策略 任务 是在算法的第4步中确定选哪两个子句做归结 以及在第5步决定这两个子句中对哪一个文字做归结主要策略 宽度优先 第一级 基本集 第二级 支持集 归结时 至少选一个是与目标公式否定式 本身或后裔 有关的子句 单元子句优先 至少有一个是单文字子句线性输入形 至少有一个是从基本子句集中挑选祖先过滤形 有一个母子句或者从基本集中挑选 或者从该母子句的先辈子句中挑选 4基于归结法的问题解答系统 4 1提取回答的方法例 ifFidogoeswhereverJohngoesandifJohnisatschool whereisFido 分析 两个已知事实和一个询问 思路 从事实出发演绎得到询问的答案 步骤 1 先用谓词公式表示问题 前提 x AT John x AT Fido x AT John School 目标 x AT Fido x 子句集 AT John x1 AT Fido x1 AT John School AT Fido x2 2 证明目标公式是前提公式集的逻辑推论3 找出一个x的例 来回答Fido在何处的询问 关键 把询问表达为一个有存在量词约束的目标公式 归结反演树 修改证明树 AT John x1 AT Fido x1 x2 x1 AT John School School x2 AT Fido x2 AT Fido x2 AT John x2 AT Fido x2 AT Fido School 例 在天花板上吊有一串香蕉的房间里 有一个可移动的箱子 问一只猴子如何规划自己的行动使得它能摘到香蕉 c a 问题描述 初始状态为S0 ONBOX AT box b AT Monkey a HB目标状态为HB 谓词的含义 1 当猴子在箱顶上时 ONBOX取真 2 当猴子拿到香蕉时 HB取真 3 谓词AT y x 当y处于x位置时取真 猴子的行为用4个规则表示 每条规则的描述形式均用谓词演算的公式组表示 P 前提条件 D 规则应用后 应从状态中删去部分 A 添加部分的状态 goto u P ONBOX x AT Monkey x D AT Monkey x A AT Monkey u Pushbox v P ONBOX x AT Monkey x AT box x D AT Monkey x AT box x A AT Monkey v AT box v ClimbboxP ONBOX x AT Monkey x AT box x D ONBOXA