chpt3-人工智能原理-逻辑系统.ppt

人工智能原理第3章逻辑系统 本章内容3 1命题逻辑和一阶谓词逻辑3 2逻辑系统的语法和语义3 3逻辑推理举例3 4逻辑智能体的推理策略参考书目附录形式系统简介 第3章逻辑系统 3 经典数理逻辑 AI研究内容之一是推理 即研究怎样使计算机获得自动推理的能力数理逻辑用数学方法研究各种推理中的逻辑问题 以推理本身作为研究对象AI要使用逻辑推理 就必然涉及数理逻辑 数理逻辑的经典部分 经典的命题逻辑和一阶谓词逻辑 同时作为人工智能的知识表示方法和推理方法而存在 因此数理逻辑是人工智能的一个基础 第3章逻辑系统 4 逻辑智能体 基于知识的智能体的核心部件是知识库 当这些知识以逻辑形式表示并进行相应的推理时 就是逻辑智能体知识表示 命题逻辑 一阶谓词逻辑推理 一阶谓词逻辑 主要有3类推理算法 前向链接和演绎系统 反向链接和逻辑程序设计 本章 归结反演和定理证明系统 第4章 采用命题和谓词演算进行推理的系统 如演绎系统 是一种典型的逻辑智能体 第3章逻辑系统 3 1命题逻辑和一阶谓词逻辑命题 真值 原子公式 合式公式谓词 论域 个体量词 变量 函数一阶语言 一阶语言的项 第3章逻辑系统 6 命题 命题 描述客观世界的可区分真假的陈述句 即判断 经典二值逻辑 非真即假 是命题的例子 2 2 4 二月份有30天 2002年哈尔滨有地震 人类能够证明数论中所有论断非真即假 有待时间 不是命题的例子 张三比李四聪明 公共汽车内非常拥挤 各人认识不同 第3章逻辑系统 7 命题变量与真值 命题变量 变元 一个命题用符号表示 称为命题符号当命题符号代表任一个命题时 即为命题变量真值 真或假 一个命题或命题变量具有真值真值连接词 5个 否定 合取 析取 蕴涵 等价 第3章逻辑系统 8 简单命题与复合命题 真值函数 真值联结词可以视为一元或二元映射 真值函数 是从 T F 到 T F 其余是 T F 2到 T F 的映射 其函数定义由真值表确定简单命题 一个被视为整体的 具有真或假的命题是简单命题 复合命题 使用联结词将简单命题联结起来的命题是复合命题 第3章逻辑系统 9 命题语言与原子公式 命题逻辑 研究复合命题之间的推导关系命题语言 是命题逻辑使用的形式语言 是符号的集合 用Lp表示 包括 命题符号 连接词 左右括号原子公式 命题语言中的一个表达式是原子公式 当且仅当它是一个命题符号 原子公式也称为文字 包括正文字和负文字 第3章逻辑系统 10 命题逻辑的合式公式 合式公式 well formedformula 简称公式 记作wff 一个表达式是一个公式 当且仅当它能通过有限次地使用下述步骤生成 1 原子公式是公式 2 如果A是公式 则 A 是公式 3 如果A B均为公式 则A B是公式 其中 表示 中的任意一个 公式的形成规则 命题逻辑的主要研究对象是公式 第3章逻辑系统 11 谓词 从命题到一阶谓词 命题内部逻辑结构的分解 对判断的分解 把判断中的具体内容抽出 称为个体 剩下的判断即为谓词谓词可看作是从个体域或个体域的笛卡儿乘积到真值集合 T F 的映射典型的推理例子 1 凡人皆有死 2 苏格拉底是人 3 苏格拉底有死 三段论式 M x D x M s D s 第3章逻辑系统 12 论域与个体 论域和个体 在一阶逻辑中 被研究对象构成的非空集称为论域 论域中的每个元素称为个体论域例子 前面例子中的论域是 人 所有的有理数都是实数 其论域为有理数一阶逻辑还研究个体之间的关系 或个体的性质 及作用于个体的函数论域 个体 个体间关系 作用于个体函数这4个成分构成了一阶逻辑的结构 第3章逻辑系统 13 谓词 谓词 关系 一阶形式语言中用于指称论域中个体的性质或者个体之间关系的形式符号 大写字母表示 给定了论域 就确定了谓词的真假值一元谓词 个体的性质 二元谓词 多元谓词 个体的关系个体的位置 空位 具体化 构成意义完整的语句空位的数目 谓词的元数 几元谓词 第3章逻辑系统 14 量词与变量 变量 变元 表示论域内的任意一个个体 常量 常元 表示确定的个体量词与变量 量词用来表示谓词的判断特性全称量词 对所有的x xP x 存在量词 存在x xP x 约束变量 中x的变量 量词所管辖的公式如P x 称为量词辖域自由变量 不在量词辖域内的变量为自由变量 第3章逻辑系统 15 约束变量和自由变量 区别 自由变量可代入常量 约束变量不行 因为 aP a 无意义 约束变量可改名 自由变量不行带有全称变量 x的命题表示为一阶公式时 其表示形式为 x P x 带有存在变量 x的命题则表示形式为 x P x 例子 所有有理数都是实数 x P x R x 有些人身高超过2米 x M x G x 上述使用方式不可改变 否则造成逻辑错误 第3章逻辑系统 16 函数 函数 表示个体之间的运算 可作用于一个或数个个体 用小写字母 给定一个或若干个体 对象 产生一个新的个体 对象 函数的元数例子 x的父亲father 张三 两数之和仍是一个数add e1 e2 第3章逻辑系统 17 函数与谓词的区别 谓词和函数的区别 谓词代表语句 结果是关系 具有真假值 函数代表关系运算 结果是一个新个体例子 谓词SUM e1 e2 e3 说明e1 e2 e3之间的关系是e1与e2的和是e3 函数add e1 e2 说明e1与e2相加的结果仍是一个数 第3章逻辑系统 18 一阶语言 1 一阶语言L 是一阶逻辑使用的形式语言 可以和任何结构 论域 没有联系 也可以与某个结构有联系与结构没有联系的一阶语言由8类符号组成 1 无限序列的个体符号 个体常量 2 无限序列的谓词符号 有确定的元数n 1有一个特殊的谓词符号称为相等符号 等式 记为 L可含或不含 如果含有 即称为含 的一阶逻辑 第3章逻辑系统 19 一阶语言 2 3 无限序列的函数符号 有确定的元数m 1 4 无限序列的自由变量 用u v w等表示自由变量 5 无限序列的约束变量 用x y z等表示约束变量 6 联结词 7 量词 8 标点 左右括号 逗号 第3章逻辑系统 20 一阶语言的项和公式 L的项 一阶语言中的一个符号是项t 当且仅当它能通过有限次使用下述步骤生成 1 个体常量 自由变量是项 2 如果t1 tn是项 且f是n元函数 则f t1 tn 是项L的原子公式 一阶语言中的一个表达式是一个原子公式 当且仅当它有如下2种形式 1 F t1 tn F是n元谓词 t1 tn是项 2 t1 t2 或t1 t2 t1 t2是项 第3章逻辑系统 21 一阶语言的公式 1 L的公式 一阶语言中的一个表达式是一个公式 当且仅当它能通过有限次使用下述步骤生成 1 原子公式是公式 2 如果A是公式 则 A 是公式 3 如果A B均为公式 则A B是公式 其中 表示 中的任意一个 4 如果A u 是公式 且x不在A u 中出现 则 xA x xA x 都是公式 第3章逻辑系统 22 一阶语言的公式 2 一阶谓词公式的例子数学命题的表示 5只被1和5整除设Q x y 表示x被y整除 N x 表示x是自然数 x Q 5 x N 5 N 1 自然语言语句的表示 他不能在所有时刻欺骗所有人设F x 表示 x是人 G x x是一个时刻 H x y 他能在y时刻欺骗x x y F x G y H x y 或者 x y H x y F x G y 第3章逻辑系统 3 2逻辑系统的语法和语义逻辑系统的语法逻辑系统的语义语法和语义之间的关系 第3章逻辑系统 24 逻辑系统 逻辑系统 亦称形式系统FormalSystem 由5个部分组成 符号表 非空集合 即逻辑 形式 语言 如一阶语言 上全体符号的集合 的子集 项和变量 的子集 公式 公式和项的交集为空公式FORMULA上的子集 公理AXIOM公式上的n元关系集合 推理规则RULE 项TERM FORMULA称为FS的组成部分 AXIOM RULE称为FS的推演部分 第3章逻辑系统 25 语法和形式推演 逻辑系统除符号表以外的部分构成了逻辑系统的语法形式推演 定义了公式之间的形式可推演性关系 它涉及公式的语法结构 其正确性能够机械地证明用记号 表示形式可推演关系 读作 推出 用 A表示A是由 形式可推演的 或形式可证明的 其中 是前提 A是结论 第3章逻辑系统 26 推演规则举例 形式推演由形式推演规则定义 举例如下 自反A A Ref 传递if Athen A 消去 反证律 if A B A Bthen A 公式变换A B A B 第3章逻辑系统 27 形式可推演性 形式可推演性 在命题 一阶逻辑系统中 A是由 可形式推演的 或形式可证明的 记为 A 当且仅当 A能通过有限次应用相应逻辑的形式推演规则生成即 A成立 当且仅当存在有限序列使得 1 A1 2 A2 n An中的每一项均由某个形式推导规则生成 且 n An就是 A即 n An A建立在上述形式推演规则基础上的形式推演系统称为自然推演 演绎 系统 第3章逻辑系统 28 逻辑系统的语义 语义即对形式语言进行解释研究可推导性即形式推演 时不考虑作为前提和结论的命题的内容 只考虑命题真假并由此确定前提的真是否蕴涵结论的真 即前提和结论之间是否有可推导关系 语法 研究形式系统的语义时 对逻辑系统赋予研究对象的集合即论域 用论域中的个体对象 对象之上的运算 函数 对象之间的关系 谓词 去解释逻辑系统中的符号 称作指称denote 指称语义学赋予形式系统的论域及解释称为形式系统的语义结构 简称结构 structure 第3章逻辑系统 29 命题逻辑的语义与可满足性 研究命题逻辑的语义 即研究公式 公式集 的真假赋值问题真假赋值 真假赋值是以所有命题符号的集合为定义域 以真假值 1 0 为值域的函数 真假赋值v给公式A指派的值记作Av可满足性 是可满足的 当且仅当有真假赋值v 使得 v 1 此时称v满足 第3章逻辑系统 30 可满足性 的可满足性蕴涵了 中所有公式的可满足性 但反过来不成立 因为这要求同一个真假赋值满足所有的公式 并非所有可满足的公式使用同一个赋值 重言式和矛盾式A是重言式 永真式 当且仅当对于任意的真假赋值v Av 1A是矛盾式 永假式 当且仅当对于任意的真假赋值v Av 0 第3章逻辑系统 31 真假判断与逻辑推论 一个命题公式是重言式或者是矛盾式或者两者都不是 需要进行判定 判定方法可通过构造真假值表方法或采用树形分支的方法来判定可推导关系 研究前提的真是否蕴涵结论的真 引入语义以后对公式进行真假赋值 如果对任意的真假赋值 都有上述关系 则说明前提和结论之间存在一种逻辑推论关系 或称逻辑蕴涵 第3章逻辑系统 32 命题逻辑的逻辑推论 逻辑推论 设 A分别是命题逻辑中的公式集合和公式 A是 的逻辑推论 记为 A 当且仅当对于任意真假赋值v v 1蕴涵Av 1 可读作 逻辑地蕴涵 是前提 和结论A之间的关系逻辑推论的证明要证明 A时 即要证明对于任何真假赋值v 如果 v 1则Av 1 通常使用反证法 第3章逻辑系统 33 一阶语言的语义 一阶语言的语义 一阶语言的解释包括一个论域和一个函数函数把一阶语言中的个体符号映射到论域中的个体n元关系符号 即谓词 映射到论域上的n元关系m元函数符号映射到论域上的m元全函数以上组成了该论域中对一阶语言的解释 第3章逻辑系统 34 一阶语言的赋值 赋值 一阶语言L的赋值v包括一个论域D和一个函数 记作v L中所有个体符号a为定义域 其赋值v a 或av关系符号F的赋值v F 或Fv函数符号f的赋值v f 或fv自由变量符号u的赋值v u 或uv则有 1 av uv D 2 Fv Dn 3 fv Dm D 第3章逻辑系统 35 一阶逻辑的逻辑推论 公式的真假值 一阶语言的公式在以D为论域的赋值之下 其真假值可以递归定义一阶逻辑的逻辑推论 与命题逻辑相同 只是这里不使用真假赋值 而用赋值逻辑推论 设 A分别是一阶语言的公式集和公式 A是 的逻辑推论 记作 A 当且仅当对于任何赋值v v 1蕴涵Av 1一阶逻辑的逻辑推论证明方法类似于命题逻辑 常用反证法 但对于否证逻辑推论 则需要构造赋值所需的论域 确定论域时 关键在于论域的大小 第3章逻辑系统 36 逻辑系统的整体特征 在经典逻辑的形式系统中 形式推演是语法概念 逻辑推论是语义概念形式系统的整体特征 是在形式系统引入语义以后 研究对于任何一阶语言的公式集 和公式A在何种赋值的条件下 其结果是否为真 即研究形式推演与逻辑推论之间的关系赋值的条件 给定某个赋值 可满足性给定任意赋值 有效性 第3章逻辑系统 37 可靠性定理与完备性定理 对于任何一阶语言的公式集 和公式A A A表示 凡是形式可推演性所反映的前提和结论之间的关系 在非形式的推理中都是成立的 即形式可推演性对于反映非形式的推理是可靠的 此即可靠性定理 或者称合理性 A A表示 凡是在非形式推理中成立的前提和结论之间的关系 形式可推演性都是能够反映的 即形式可推演性在反映非形式推理时没有遗漏 此即完备性定理 第3章逻辑系统 38 可满足性与有效性 1 不加证明地给出有关定义和定理可满足性 一阶逻辑公式集合 是可满足的 当且仅当有 以某个不空集为论域 赋值v 使得 v 1 当 v 1时 称v满足 反过来 不可满足性就是对任意论域上的任意赋值都有 v 0 第3章逻辑系统 39 可满足性与有效性 2 有效性 一阶逻辑公式A是有效的 当且仅当对于 以任何不空集为论域 任何赋值v Av 1 有效性也称为普遍有效性论域中的可满足性 有效性 1 在D中是可满足的 当且仅当有以D为论域的赋值v 使得 v 1 2 A在D中是有效的 当且仅当对于任何以D为论域的赋值v Av 1 第3章逻辑系统 40 可满足性与有效性 3 关于命题的 定理 1 A是可满足的 当且仅当 A是不有效的 2 A是有效的 当且仅当 A是不可满足的 关于一阶的 定理 1 A u1 un 是可满足的 当且仅当 x1 xnA x1 xn 是可满足的 2 A u1 un 是有效的 当且仅当 x1 xnA x1 xn 是有效的 第3章逻辑系统 41 可靠性定理 可靠性定理 1 设 Form L A Form L 也包括了命题语言Lp 1 如果 A 则 A 2 如果 A 则 A 即所有形式可推演的都是有效的 协调性 无矛盾性 Form L 是协调的 当且仅当不存在A Form L 使得 A且 A可靠性定理 2 设 Form L A Form L 1 如果 是可满足的 则 是协调的 2 如果A是可满足的 则A是协调的 1 2 等价 第3章逻辑系统 42 完备性定理 命题逻辑和一阶逻辑的完备性定理 1 设 Form L A Form L 含Lp 1 如果 是协调的 则 是可满足的 2 如果A是协调的 则A是可满足的 定理 2 设 Form L A Form L 1 如果 A 则 A 2 如果 A 则 A 所有有效公式都是形式可证明公式 如果对论域限定以后 可得更精确的陈述 第3章逻辑系统 3 3逻辑推理举例wumpus世界命题逻辑推理模式基于电路的智能体 第3章逻辑系统 44 wumpus世界 1 Wumpus是一个早期电脑游戏中的怪物Agent感知 陷阱旁边有微风breeze怪兽旁边有恶臭stench金子闪闪发光glitter感觉墙的反弹陷阱和怪物的位置随机生成 第3章逻辑系统 45 wumpus世界 2 Wumpus世界搜索图示 感知用5元组表示 感知wumpus 感知微风 感知金光 感知墙 感知wumpus被杀死 A AgentB BreezeG Glitter GoldOK safesquareP PitS StenchV visitedW wumpusN None 第3章逻辑系统 a N N N N N b N B N N N 46 wumpus世界 3 第3章逻辑系统 A AgentB BreezeG Glitter GoldOK safesquareP PitS StenchV visitedW wumpusN None c S N N N N d S B G N N 47 wumpus世界中的命题和推理规则 只考虑陷阱的情况Pi j T i j 中有陷阱 记为Pi jBi j T i j 中有微风 记为Bi j规则如下 R1 P1 1R2B1 1 P1 2 P2 1R3B2 1 P1 1 P2 2 P3 1R4 B1 1R5B2 1 第3章逻辑系统 48 命题逻辑推理模式 分离规则与消去逻辑等价 双向蕴涵消去 第3章逻辑系统 49 wumpus世界的推理例子 用R1 R5规则和推理模式证明 1 2 和 2 1 中没有陷阱 即 P1 2和 P2 1证明 从R2开始R6 B1 1 P1 2 P2 1 P1 2 P2 1 B1 1 R2双向蕴涵消去R7 P1 2 P2 1 B1 1R6与消去R8 B1 1 P1 2 P2 1 逆否命题逻辑等价R9 P1 2 P2 1 R4 R8分离规则R10 结果 P1 2 P2 1迪摩根定律 第3章逻辑系统 50 基于电路的智能体 基于电路的智能体的目的 把对现状的感知变为智能体的行动感知 input 判断 行动判断 尖叫 怪兽wumpus将死亡行动 金光 抓起金子 行动控制 寄存器 第3章逻辑系统 grab glitter Alive 延迟 Scream 51 wumpus世界中智能体的判断 1 位置判断 在L1 1 分为3种情况 一直留在 1 1 从 1 2 走到 1 1 从 2 1 走到 1 1 使用位置寄存器 状态寄存器 第3章逻辑系统 L1 2 L2 1 facing left facing down L1 1 forward bump 52 wumpus世界中智能体的判断 2 上述电路图表示为逻辑表达式 第3章逻辑系统 前述电路的逻辑表达式判断wumpus是否活着发现金子后的行动但因为没有变量 不能表示更一般的情况 如不同位置用同一个逻辑式 3 4逻辑智能体的推理策略逻辑智能体构造Horn子句置换与合一前向链接算法 后向链接算法 第3章逻辑系统 54 逻辑智能体的构造 1 以一阶谓词演算为核心的逻辑系统是典型的逻辑智能体系统的基础是一阶语言 由此构造知识库 一般构造知识库 知识工程 的过程包括 确定任务收集相关知识确定谓词 函数和常量词汇表 第3章逻辑系统 55 逻辑智能体的构造 2 对领域 论域 的通用知识进行编码对特定问题实例的描述进行编码查询提交 推理 给出答案调试知识库如果采用一阶语言的特殊形式 确定子句Horn子句 可获得高效推理 第3章逻辑系统 56 Horn子句 Horn子句 HornClause 是一类至多只有一个正文字的子句 子句 文字的析取式 例子 A B C 注意 这是一般公式A B C的变形 Horn子句称为确定子句 其中正文字称为子句的头 负文字构成子句的体 第3章逻辑系统 57 Horn子句的性质 只有一个正文字的约束具有重要意义 每个Horn子句实际上都是一个蕴涵式的变形 实际知识库中常常使用这样易懂的形式 没有正文字的Horn子句可以写成结论为FALSE的蕴涵式Horn子句的推理可以使用前向链接和后向链接算法用Horn子句判定蕴涵所需时间与数据库成线性关系最重要的是最后一个性质 第3章逻辑系统 58 推理策略 简要介绍2种推理算法 简单的前向链接算法和简单的后向链接算法 结合一个例子说明算法的应用一阶推理规则 一般化分离规则 GeneralizedModusPonens 对于原子语句pi pi q 存在置换 使得 pi pi 对所有i都成立 则 第3章逻辑系统 59 置换与合一 置换 或代换 设x1 xn是n个变量 且各不相同 t1 tn是n个项 常量 变量 函数 ti xi 则有限序列 t1 x1 t2 x2 tn xn 称为一个置换置换乘积 合成 设 和 是2个置换 则先 后 作用于公式或项 称为置换乘积 用 表示 通过相关的置换 使不同的一阶公式成为一样的 这个过程称为合一 第3章逻辑系统 60 合一置换 合一置换 设有一组谓词公式 E1 Ek 和置换 使E1 E2 Ek 则 称为合一置换 E1 Ek称为可合一的 合一置换也叫通代最一般合一置换 最广通代 如果 和 都是公式组 E1 Ek 的合一置换 且有置换 存在 使得 则 称为公式组 E1 Ek 的最一般合一置换 记为mgu mostgeneralunification 第3章逻辑系统 61 置换与合一的例子 有子句 xKing x Greedy x Evil x King John Greedy John 则做置换 x John 用一般化分离规则可得 q Evil John 第3章逻辑系统 62 合一结果 对于合一UNIFY 合一的结果是一个置换 如 UNIFY Know John x Know John Jane x Jane UNIFY Know John x Know y Mary x Mary y John 但是UNIFY K John x K x Jane FAIL 原因是x不能同时选取2个值详细的合一算法将在第6章介绍 第3章逻辑系统 63 用于逻辑推理的例子 问题描述 美国法律规定 美国人 American 卖武器 weapon 给敌对国家 hostile 是犯罪的 criminal 美国的敌国Nono有一些导弹 missile 所有这些导弹是West上校卖给他们的 而West上校是一个美国人证明 West是犯罪的 第3章逻辑系统 64 问题用一阶子句表示 1 用确定子句表示上述内容美国人卖武器给敌对国家是犯罪的American x Weapon y Sell x y z Hostile z Criminal x 1 Nono有一些导弹 xOwn Nono x Missile x 消去其中的存在量词 引入新常量 得到2个原子公式 正文字 Own Nono M1 4 Missile M1 5 第3章逻辑系统 65 问题用一阶子句表示 2 所有该国导弹都是West上校出售的Missile y Own Nono y Sell West y Nono 2 导弹是武器Missile y Weapon y 3 其它陈述 美国人WestAmerican West 6 敌国NonoHostile Nono 7 上述描述放入知识库 1 3 为确定子句 上述原始形式均可以化为原子的析取且只有一个正文字 4 7 为正文字 第3章逻辑系统 66 前向链接算法的说明 1 前向链接算法的推理过程 从已知事实 知识库中的原子公式 开始 依次对知识库中的规则 以确定子句的形式出现 进行置换 检查规则前提部分的文字是否全部与知识库中的事实相匹配如果是匹配的 则把该条规则已经做过置换的结论部分添加到知识库中 如果这个结论和查询 既需要推导出的结论 一致 则推理结束 获得证明 第3章逻辑系统 67 前向链接算法的说明 2 重复上述过程 直到获得证明 或者再没有新的事实 推出的结论 加入 则此时推理以证明失败结束约束 要求每次加入知识库的结论都是全新的 而不是已知事实的重命名 即谓词相同只是变量名不同 第3章逻辑系统 68 简单的前向链接算法 FunctionFC KB ReturnasubstitutionorFALSEInputs KB asetoffirst orderdefiniteclauses thequery anatomlocalvariables new thenewrulesinferredoneachiterationrepeatuntilnewisemptynew foreachruler intheformofdefineclause inKBdoforeach suchthat p1 pn p1 pn get q q ifq isnew satisfiedtheconstraint thendoaddq tonew UNIFY q If isnotfailthenreturn addnewtoKBreturnfalse 第3章逻辑系统 69 前向链接算法例子 1 第3章逻辑系统 使用前向链接算法对前面的例子进行推理用知识库中的事实 即 4 7 依次对知识库中的各个子句进行置换操作并用推理规则获得新的文字第一次循环体执行 子句 1 前提部分未获满足 为什么 子句 2 使用置换 x M1 则可得Sell West M1 Nono 8 子句 3 使用置换 x M1 则可得Weapon M1 9 70 前向链接算法例子 2 第3章逻辑系统 此时new中为 8 9 为原知识库所未有 将它们添加到知识库中第二次循环体执行 再次循环时new首先清空子句 1 置换 x West y M1 z Nono 得到Criminal West 10 添加到new中 与查询进行合一测试 一致则返回 算法结束 71 前向链接生成的证明树 第3章逻辑系统 72 反向链接算法的说明 1 原始查询 既要证明的结论 以目标列表的形式出现 开始时列表中只有一个元素列表的操作相当于栈 是一个递归过程 如下 即深度优先的搜索过程推理过程是从结论 子句的头 开始 找到匹配的头就扩展这个头所在的规则体 扩展部分又作为头继续扩展 直到全部原子均与事实相匹配比较 正向 事实 结论 反向 结论 事实 第3章逻辑系统 73 反向链接算法的说明 2 算法的推理过程是 选取栈当中的第一个目标 在知识库中寻找子句的头 即结论部分 能与目标合一的每个子句每个这样的子句创建了一个递归调用过程 在这个递归调用过程中子句的前提 子句的体 被加入到目标栈当中当栈中所有目标都得到匹配 则当前的证明分支是成功的注意 事实是指有头没有体的子句 正文字 第3章逻辑系统 74 反向链接算法的说明 3 在算法中answers作为存放置换的数据结构 返回一系列置换操作 这些操作说明了反向链接算法获取证明的过程在算法中包括了置换的合成 或者写为Compose 其效果就是依次进行每个置换 第3章逻辑系统 75 反向链接算法的说明 4 第一次应用算法 对于待证明的目标来说 本身就是一个正文字 此时要用这个文字中的常量对合适的规则 子句的头与该文字匹配 进行置换这个置换通过递归调用带入下一次置换 就得到了合成置换在本例中有 初始 x West 递归 x West y M1 递归 x West y M1 z Nono 第3章逻辑系统 76 简单的反向链接算法 FunctionBC KB goals returnsasetofsubstitutionsInputs KB goals alistofconjunctsformingaquery alreadyapplied thecurrentsubstitution initial localvariables answers asetofsubstitutions initial ifgoalsisemptythenreturn q FIRST goals 初始为空 递归以后不空 foreachruler intheformofdefineclause inKBand UNIFY q q succeedsnew goal p1 pn asREST goals answers BC KB new goal answersreturnanswers 第3章逻辑系统 77 反向链接算法例子 1 反向链接算法推理过程目标Criminal West 分解为公式 1 前提部分的4个文字 即American West Weapon y Sell West y z Hostile z 置换 x West American West 和事实相匹配需要递归匹配 Weapon y Sell West y z Hostile z Weapon y 递归调用前 x West 进入第一次递归产生Missile M1 此时置换 y M1 匹配 递归返回复合 x West y M1 第3章逻辑系统 78 反向链接算法例子 2 再次递归调用Sell West M1 z 得到置换 z Nono 递归返回复合置换 x West y M1 z Nono 在置换过程中每个变量只能置换一个常量作为约束 减少置换的不定性此时子目标全部匹配 再无新的子目标生成 返回置换集合结束 第3章逻辑系统 79 反向链接生成的证明树 第3章逻辑系统 80 正向链接和反向链接 前向链接算法特点 数据驱动 是可靠的和完备的后向链接算法特点 目标驱动 是可靠的但不是完备的 书中p220 p224 可以从 是否能找到问题的解 角度考虑不完备性后向链接算法根据目标来进行相关事实的匹配 对于大规模的知识库来说有助于减小搜索空间 第3章逻辑系统 81 参考书目 StuartRussell PeterNorvig AIMA第7章 第8章 第9章陆汝钤编著 人工智能 上册 第1章陆钟万 面向计算机科学的数理逻辑 科学出版社 1998年1月第1版朱梧 木贾 肖奚安 数理逻辑引论 南京大学出版社 1995年5月第1版王元元 计算机科学中的逻辑学 科学出版社 1989年9月第1版 第3章逻辑系统 附录形式系统简介F1形式系统和形式推演F2形式系统的语义F3形式系统的整体特征 第3章逻辑系统 F1形式系统定义和形式推演 第3章逻辑系统 84 形式系统定义 1 逻辑的形式系统的定义 一个形式系统FormalSystem由5个部分组成 1 符号表 非空集合 即形式语言 如Lp和L 2 上全体符号的集合 的一个子集TERM 其元素称为FS的项 TERM有子集VARIABLE 其元素称为变量 3 的一个子集FORMULA 其元素称为FS的公式 FORMULA有子集ATOM 其元素称为原子公式 TERM FORMULA 第3章逻辑系统 85 形式系统定义 2 4 FORMULA的一个子集AXIOM 其元素称为FS的公理 5 FORMULA上的n元关系集合RULE 其元素称为FS的推理规则 其中 TERM FORMULA称为FS的组成部分 AXIOM RULE称为FS的推演部分公理推演系统包括AXIOM 而自然推演系统只包括推理规则 第3章逻辑系统 86 对象语言和元语言 1 对象语言和元语言 作为被研究对象的语言称为对象语言 用以研究对象语言的语言称为元语言例子 用汉语研究英语语法 则英语是对象语言 汉语是元语言数理逻辑中的形式系统各有其自身的形式语言如Lp和L 这些是被研究的对象 因而是对象语言 但为了研究这些形式系统 又必须使用某种语言 那么这种语言便是元语言 第3章逻辑系统 87 对象语言和元语言 2 如 鸟正在飞翔 描述 对象语言 命题 鸟正在飞翔 真 对上句的评论 元语言 形式系统的对象语言 其中的符号既是对客观对象的抽象 用于研究客观对象 同时又是一种符号客体 是被研究的对象 第3章逻辑系统 88 对象语言和元语言 3 形式系统的元语言包括 对形式系统中组成成分的称谓 项 公式 公理等逻辑术语 如果 那么 当且仅当 存在 所有等对形式系统性质 整体特征 的描述 如一致性 完备性 可判定性等 该部分最重要元语言中使用的符号 自然语言 如汉语 和一些被引进的符号 如 等未经解释的形式语言可以没有含义 但元语言必须有其具体含义 第3章逻辑系统 89 元理论 元理论是关于形式系统的理论 包括三部分内容 关于形式系统语法 syntax 的研究 不涉及具体意义的符号体系 研究符号串的推演 即形式推演 关于形式系统语义 semantics 的研究 研究形式系统在被作出各种解释时的性质 关于形式系统语法和语义关系的研究 特别是形式系统的性质 如 合理性 完备性等 第3章逻辑系统 90 形式推演 形式推演 定义了公式之间的形式可推演性关系 它涉及公式的语法结构 其正确性能够机械地证明用记号 表示形式可推演关系 读作 推出 用 A表示A是由 形式可推演的 或形式可证明的 其中 是前提 A是结论记号 不是形式语言中的符号 A也不是形式语言中的公式 而是元语言中的命题 第3章逻辑系统 91 常用推演规则 1 形式推演由形式推演的规则定义命题逻辑中有一些常用的推演规则 规则模式 肯定前提ifA then A 增加前提if Athen A 自反A A Ref 传递if Athen A 第3章逻辑系统 92 常用推演规则 2 消去 反证律 if A B A Bthen A 引入 归谬律 if A B A Bthen A 消去if A B Athen B 引入if A Bthen A B 第3章逻辑系统 93 常用推演规则 3 消去if A Bthen A B 引入if A Bthen A B 消去if A C B Cthen A B C 引入if Athen A B B A 第3章逻辑系统 94 常用推演规则 2 消去if A B Athen Bif A B Bthen A 引入if A B B Athen A B 通过连接词的增减或变形 实现公式的变换常用A B A B 第3章逻辑系统 95 形式可推演性 1 命题逻辑 形式可推演性 在命题逻辑中 A是由 可形式推演的 或形式可证明的 记为 A 当且仅当 A能通过有限次应用命题逻辑的形式推演规则生成即 A成立 当且仅当存在有限序列使得 1 A1 2 A2 n An中的每一项均由某个形式推导规则生成 且 n An就是 A即 n An A 第3章逻辑系统 96 形式可推演性 2 用 A表示 A不成立用A B表示左右两边的公式可以互相推出 称其为语法等值公式或等值公式建立在上述形式推演规则基础上的形式推演系统称为自然推演 演绎 系统 第3章逻辑系统 97 形式可推演性 3 命题逻辑中的形式推演规则都包括在一阶逻辑当中 但是其中出现的公式是一阶语言中的公式 另外增加了关于量词的规则 一阶逻辑 形式可推演性 在一阶逻辑中 A是由 可形式推演的 或形式可证明的 记为 A 当且仅当 A能通过有限次应用一阶逻辑的形式推演规则生成形式推演的例子可以参考本章后面列出的3本关于逻辑的教科书 第3章逻辑系统 F2形式系统的语义 第3章逻辑系统 99 形式系统的语义 1 语义即对形式语言进行解释研究可推导性即形式推演 时不考虑作为前提和结论的命题的内容 只考虑命题真假并由此确定前提的真是否蕴涵结论的真 即前提和结论之间是否有可推导关系 语法 研究形式系统的语义时 对形式系统赋予研究对象的集合即论域 用论域中的个体对象 对象之上的运算 函数 对象之间的关系 谓词 去解释形式系统中的符号 称作指称denote 指称语义学 第3章逻辑系统 100 形式系统的语义 2 赋予形式系统的论域及解释称为形式系统的语义结构 简称结构 structure 结构及其在该结构下公式所取真值的规定 称为形式系统的指称语义 denotationalsemantics 第3章逻辑系统 101 命题逻辑的可满足性 研究命题逻辑的语义 即研究公式 公式集 的真假赋值问题真假赋值 真假赋值是以所有命题符号的集合为定义域 以真假值 1 0 为值域的函数 真假赋值v给公式A指派的值记作Av可满足性 是可满足的 当且仅当有真假赋值v 使得 v 1 此时称v满足 第3章逻辑系统 102 可满足性 的可满足性蕴涵了 中所有公式的可满足性 但反过来不成立 因为这要求同一个真假赋值满足所有的公式 并非所有可满足的公式使用同一个赋值 重言式和矛盾式A是重言式 永真式 当且仅当对于任意的真假赋值v Av 1A是矛盾式 永假式 当且仅当对于任意的真假赋值v Av 0 第3章逻辑系统 103 真假判断与逻辑推论 一个命题公式是重言式或者是矛盾式或者两者都不是 需要进行判定 判定方法可通过构造真假值表方法或采用树形分支的方法来判定可推导关系研究前提的真是否蕴涵结论的真 引入语义以后对公式进行真假赋值 如果对任意的真假赋值 都有上述关系 则说明前提和结论之间存在一种逻辑推论关系 或称逻辑蕴涵 此时对关系陈述得也更精确 第3章逻辑系统 104 命题逻辑的逻辑推论 逻辑推论 设 A分别是命题逻辑中的公式集合和公式 A是 的逻辑推论 记为 A 当且仅当对于任意真假赋值v v 1蕴涵Av 1 可读作 逻辑地蕴涵 是前提 和结论A之间的关系 但不是命题语言中的符号 A是元语言中的命题 第3章逻辑系统 105 逻辑推论的证明 逻辑推论的证明要证明 A时 即要证明对于任何真假赋值v 如果 v 1则Av 1但任意的真假赋值难于验证故使用反证法 假设 A 即存在一个真假赋值v 使得 v 1且Av 0 由此而产生矛盾 即肯定了 A 第3章逻辑系统 106 一阶语言的语义 1 一阶语言的语义 一阶语言的解释包括一个论域和一个函数 函数把一阶语言中的个体符号 n元关系符号 即谓词 m元函数符号分别映射到论域中的个体 论域上的n元关系和m元全函数 是在这个论域中对一阶语言的解释 第3章逻辑系统 107 一阶语言的语义 2 如果n元关系符号和m元函数中不含自由变量 其项为论域中的个体ai 则原子公式F t1 tn 被解释为 a1 an有R关系 项f t1 tn 被解释为论域中的个体f a1 an 对于含有自由变量的函数 项 和公式 则分别被解释为论域上的m元函数和n元命题函数 它们经过解释 再给其中的自由变量符号指派论域中的某些个体 就得到论域中个体作为其值 真或假的命题作为其真假值 第3章逻辑系统 108 一阶语言的赋值 1 赋值 一阶语言L的赋值v包括一个论域和一个函数 记作v 以L中所有个体符号a 关系符号F 函数符号f和自由变量符号u构成的集合为定义域 且分别把v a v F v f v u 写作av Fv fv uv 则有 1 av uv D 2 Fv Dn 3 fv Dm D 第3章逻辑系统 109 一阶语言的赋值 2 项的值 在以D为论域的赋值v之下的项的值递归定义如下 1 av uv D 2 f t1 tn v fv t1v tnv 对于一阶语言的项t 设v是以D为论域的