人工智能谓词演算.ppt

第2讲基于谓词逻辑的机器推理 一阶谓词逻辑归结演绎推理归结原理的应用Horn子句与Prolog程序设计 2 第一节一阶谓词逻辑 命题 凡可确定真假的陈述句称为命题可以取值 真 T 或 假 F 在一定的条件下 只能取其中一个值例 1 北京是中国的首都 2 3 2 10 3 1 11 100 根据制数 4 禁止吸烟 祈使句 5 本命题是假的 悖论 3 谓词 是用来刻画个体词的性质或个体词之间的关系的词 带参量的命题叫谓词 n元谓词 P x1 x2 x3 xn P是谓词符号 代表一个确定的特征 一个参量 或关系 多个参量 x1 x2 x3 xn称为参量或项 个体常元或个体变元 论述域 个体域 个体变元的取值范围例 北京是一个城市 CITY 北京 x是人 HUMAN x A是B的兄弟 兄弟 A B x大于y G x y 不带个体变元的谓词公式叫命题 命题是谓词公式的特例 4 逻辑连接词 研究单个谓词是不够的 还必须研究多个谓词之间的关系 这需要引入逻辑连接词 否定词 A读为 非A 当A为真时 A为假 当A为假时 A为真 合取词A B读为 A并且B 当且仅当A和B都为真时 A B为真 否则A B为假 析取词A B读为 A或者B 当且仅当A和B都为假时 A B为假 否则A B为真 5 蕴涵词A B读为 若A则B 当且仅当A为真 且B为假时 A B为假 否则A B为真在A B中 A称为前件 B称为后件 等值词A B读为 A等值于B 当且仅当A和B同为真或同为假时 A B为真 否则A B为假 6 量词 有些陈述句包含表示数量的词 如 所有 任一 存在 至少有一个 等 为了表示这样的陈述句 需引入新的符号 称为量词全称量词 x 表示 对于所有的x 例 凡是人都有名字 x M x N x x A x A a1 A a2 A an 若论域为有限集合 且a1 a2 an是论域中的所有个体存在量词 x 表示 对于某个x 例 存在不是偶数的整数 x G x E x x A x A a1 A a2 A an 例 见P56例1 3 7 项 P64定义1 1 个体常元和个体变元都是项 2 f t1 t2 tn 是项 f是n元函数 t1 t2 tn是项 3 只有有限次使用 1 2 得到的符号串才是项原子公式 P64定义2 设P为n元谓词符号 t1 t2 tn是项 则P t1 t2 tn 称为原子谓词公式 简称原子公式 8 谓词公式 P56定义3 1 原子公式是谓词公式 2 若A B是谓词公式 则A B A B A A B A B xA xA也是谓词公式 3 只有有限次应用 1 2 生成的公式才是谓词公式谓词公式又称为谓词逻辑中的合式公式 记为Wff well formedformula 几个概念 辖域 P57 紧接于量词之后被量词作用的 说明的 谓词公式称为该量词的辖域指导变元 约束变元和自由变元 P57 改名规则 P57 保证一个变元或者是约束变元 或者是自由变元例 x H x G x y xA x B x 9 合取范式 P58定义4 A为合取范式 B1 B2 Bn 其中Bi形如L1 L2 Lm Lj为原子公式或其否定例 P x Q y P x Q y R x y 任一谓词公式均可化为与之等价的合取范式 但一般不唯一析取范式 P66定义5 A为析取范式 B1 B2 Bn 其中Bi形如L1 L2 Lm Lj为原子公式或其否定例 P x Q y P x Q y R x y 任一谓词公式均可化为与之等价的析取范式 但一般不唯一 10 谓词公式的永真 有效 永假 不可满足 可满足 P58定义6 7 与个体域有关谓词公式之间的关系常用逻辑等价式P59表3 1注意 与 的区别 是等价符号 说明两个谓词公式之间的等价性 是逻辑连接词 是谓词公式的组成部分常用逻辑蕴涵式P60表3 2注意 与 的区别 是推导符号 说明由 左边的谓词公式可以推导出 右边的谓词公式 是逻辑连接词 是谓词公式的组成部分 11 自然演绎推理 1 将自然语言命题转化为谓词公式 2 利用上面的逻辑等价式和逻辑蕴涵式 可以进行推理 得出一些隐含在谓词公式中的结论例 P61例4 6自然演绎推理实施困难 推理规则太多 应用规则需要很强的模式识别能力 中间结论呈指数增长引入新的推理技术 归结演绎推理技术归结 消解 Resolution 由Robinson于1965年提出 大大推动了自动定理证明的发展 12 练习 1 设已知以下事实 ABA CB C DD Q求证 Q为真 13 证明 因为A A C CB C B CB C B C D DD D Q Q所以Q为真 14 2 设已知如下事实 1 凡是容易的课程小王都喜欢 2 C班的课程都是容易的 3 ds是C班的一门课程 求证 小王喜欢ds这门课程 15 证明 事实 x EASY x LIKE Wang x x C x EASY x C ds LIKE Wang ds 因为 x C x EASY x 所以C ds EASY ds 所以C ds C ds EASY ds EASY ds 因为 x EASY x LIKE Wang x 所以EASY ds LIKE Wang ds 所以EASY ds EASY ds LIKE Wang ds LIKE Wang ds 16 第二节归结演绎推理 建立子句集文字 子句 空子句 P62定义1 建立谓词公式G的子句集合 P62定义2 例 P62例3 7例 P63例2有关消去存在量词子句集中各子句的关系是合取 经过变换后的子句集S 与谓词公式G并不等价子句集的不可满足 P64定义3 G不可满足当且仅当S不可满足 P64定理1 即G永假是S永假的充分必要条件 17 练习 P931 1 p x y Q u v 2 p x y Q x y 3 P x f x Q x f x R x f x 4 P x z Q x y R x y 5 P a b z f z v g z v Q a b f t s g t s R a t g t s 18 命题逻辑中的归结原理在定理证明系统中 已知一公式集F1 F2 Fn 要证明W 定理 是否成立 即要证明W是公式集的逻辑结果 有两种方法 1 证明F1 F2 Fn W为永真式 见上一节 2 反证法 证明F1 F2 Fn W永假 即要证明对应子句集永假 不可满足 几个概念 P64定义4 5 互补文字 归结式 消解式 亲本子句 消解基例 例3 9归结式是其亲本子句的逻辑结果P64定理2单向推导关系 19 归结原理 C1 C2 C1 L1 C2 L2 互补文字进行归结得空子句 L L 另L L F 假 故空子句即永假子句关于消解前后子句集的可满足性 P65推论 证明略 故 要证明一子句集永假 可以通过对子句集应用消解原理得到空子句来证明运用归结原理证明定理的例子 P65例11 12 归结过程可以用一棵归结演绎树表示 20 替换与合一为了对谓词逻辑的子句集运用消解原理 即在子句集合中寻找含互补文字的子句对 必须对子句进行替换合一操作替换 P66定义6 t1 x1 t2 x2 tn xn 对表达式的替换过程P66定义7表达式 项 原子公式 文字 子句两个替换的乘积P66 67定义8一部分仍是 的替换对 只是 的项被 作了替换 另一部分是 中与 不同的那些变量对例 例3 13替换的乘积满足结合律 21 合一 P67定义9 是S的一个合一其中S是一个原子谓词公式集 是一个替换满足F1 F2 Fn 一个公式集的合一一般不唯一最一般的合一 P67定义10 是S的一个合一对于S的任何一个合一 存在替换 使 称 为S的最一般 最普通 最简单 合一MGU例 例3 14MGU的替换限制最少 所产生的例更一般化 这有利于归结过程的灵活使用一个公式集的最一般合一也可不唯一 如 P x P y y x x y 都是它的最一般合一 22 差异集 P67定义11针对具有相同谓词名的原子公式集例 例3 15合一算法 求非空有限具有相同谓词名的原子公式集的最一般合一P67 68合一算法是解决两个表达式匹配的问题 两个表达式都可以含有变量 通过算法求得MGU并进行替换后就可以得到匹配的例例 例16 17合一定理 P68 69定理3可合一公式集一定存在最一般合一 用上述合一算法求得 23 谓词逻辑中的归结原理归结过程 若S中的两子句间有相同互补文字的谓词 但它们的项不同 则必须找出对应的不一致项进行变量替换合一操作 使它们的对应项一致求归结式看能否导出空子句几个概念 P69定义12 谓词逻辑中的二元归结式 二元消解式 亲本子句 消解文字例 例18 19子句用文字的集合表示 各文字之间的关系是析取 首先对子句内部的可合一文字进行合一 24 因子 单因子 P69定义13 例 例14子句的归结 消解 式 P69定义14 定理 谓词逻辑中的消解式是它的亲本子句的逻辑结果谓词逻辑中的归结原理 C1 C2 C1 L1 C2 L2 关于消解前后子句集的可满足性 P70 同命题逻辑 故 要证明F1 F2 Fn W为永真式 可证明F1 F2 Fn W永假 这又可以通过对对应子句集应用消解原理得到空子句来证明 同命题逻辑 25 例 例15 16定理 归结原理的完备性 P71 练习 P933 1 5 26 第三节归结原理的应用 例3 23 P71例3 24 P72练习 P945 6 27 归结策略计算机实现归结原理的一般算法 1 将子句集S置入CLAUSES表 2 若空子句NIL在CLAUSES中 则归结成功 结束 3 若CLAUSES中存在可归结子句对 则归结之 并将归结式放入CLAUSES中 4 归结失败 退出 归结策略的完备性策略 删除策略 支持集策略 线性归结策略 输入归结策略 单元归结策略 祖先过滤形策略 28 归结举例 Sam Clyde和Oscar是大象 关于它们 我们知道以下事实 1 Sam是粉红色的 2 Clyde是灰色的且喜欢Oscar 3 Oscar是粉红色或者是灰色 但不是两种颜色 且喜欢Sam 用归结法证明一个灰色大象喜欢一个粉红色大象 即证明 x y Gray x Pink y Likes x y 谓词 Gray x Pink x Like x y 事实 1 Pinky Sam 2 Gray Clyde Like Clyde Oscar 3 Gray Oscar Pink Oscar Likes Oscar Sam 29 子句集 1 Pink Sam 2 Gray Clyde 3 Like Clyde Oscar 4 Gray Oscar Pink Oscar 5 Likes Oscar Sam 6 Gray x Pink y Likes x y 归结 7 Gray Oscar Pink Sam 5 6得8 Gray Clyde Pink Oscar 3 6得9 Pink Oscar Pink Sam 4 7得10 Pink Oscar 8 2得11 Pink Sam 9 10得12 NIL1 10得 30 第四节Horn子句与Prolog程序设计 子句的蕴含表示P90 3 1 3 4 4 4 蕴含型子句的归结P90 91正 负文字归结 在 的两头去找 Horn子句定义 P91定义1蕴含型Horn子句的三种类型 P91蕴含型Horn子句的归结例 P91例1注意归结顺序 31 Prolog程序设计P30Prolog程序的语句均是Horn子句事实 无条件子句规则 条件子句问题 目标子句Prolog程序P31 33Prolog程序的运行机制P33 35SLD归结 从目标子句开始进行归结归结顺序是从左到右控制策略是深度优先有回