谓词逻辑与归结原理.ppt

3.3.6 归结过程 例：设任何通过计算机考试并获奖的人都是快乐的；任何肯学习或幸运的人都能通过所有的考试；张不肯学习但他是幸运的；任何幸运的人都能获奖。求证：张是快乐的 定义谓词： Pass(x,y) 表示x通过y考试 Win(x,prize) 表示x能获奖 Lucky(x) 表示x是幸运的 Study(x) 表示x肯学习 Happy(x) 表示x是快乐的 * 3.3.6 归结过程 写出谓词公式： 前提： 结论：Happy(zhang) ，取否 ~ Happy(zhang) 证明：对前提和结论分别求子句 * 3.3.6 归结过程 得到两个子句 * 3.3.1 归结原理 归结： 1、 ~P∨~Q∨R 2、 ~ P ∨ Q 3、P 4、~R 5、 ~P∨R 1、2归结 6、 R 3、5归结 7、 □ 4、6归结 因此得证 * 子句集为：{~P∨~Q∨R, ~ P ∨ Q, P, ~R} 3.3.1 归结原理 步骤 命题逻辑归结原理 谓词逻辑归结原理 1、建立A∧~B 命题逻辑公式 谓词逻辑公式 2、求子句集 求合取范式 求前束合取范式 消去量词 3、归结 直接消去互补项 利用置换与合一消去互补项 归结式加入子句集 归结式加入子句集 * 3.3.1 归结原理 谓词逻辑归结原理的重点 如何对前束合取范式消去量词 命题逻辑 谓词逻辑 如何利用置换与合一对不同变量的子句进行置换 命题逻辑 谓词逻辑 * 3.3.1 归结原理 求前束合取范式： 方法一：先转化为前束范式，再将辖域中的谓词公式转化为合取范式 方法二： (1)消去联结词→ 和?。 (2)将联结词~向内深入，使之只作用于原子公式。 (3)利用换名或替代规则使所有约束变元的符号都不同，并且自由变元与约束变元的符号也不同。 (4)利用量词辖域的扩张和收缩，扩大量词至整个公式。 (5)再将辖域中的谓词公式转化为合取范式。 * 3.2.3 谓词演算与推理 量词辖域收缩与扩张等值式 * 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、辖域中的公式化为合取范式 * 3.3.2 Skolem标准型 例 求前束合取范式 * 3.3.2 Skolem标准型 Skolem标准型：对前束合取范式消去所有的量词。P100 第一步：消去存在量词? ： 1、如果?之前(左边)没有任意量词?, 则用常量替换?的指导变量 可用常量b替换x消去存在量词，得P(b,a) 2、如果?之前(左边)有任意量词? ，则用任意量词的函数替换?的指导变量 可用f(x)替换y消去存在量词， 第二步消去任意量词?：简单的省略即可 * 3.3.2 Skolem标准型 例： 1、消去存在量词?y和 ?u ： ?y 前面有任意量词，指导变量为x，因此用f(x)替换y， ?u前面有任意量词，指导变量为x，因此用g(x)替换u 2、消去任意量词： * 3.3.2 Skolem标准型 例 判断下列的消去量词的过程是否正确。 证明： ① ?x ?y G(x, y) ② ? y G(x, y) 消去 ?x ③ G(x, a) 消去 ?y 对任意x，都存在一个恒定常量a，使G(x, a) 成立 ① ?x ?y G(x, y) ② ?x G(x, f(x)) 消去 ?y ③ G(x, f(x)) 消去 ?x 对任意x， 都存在一个与之对应的f(x)，使G(x, f(x)) 成立 * 3.3.3 子句集 定义 文字：不含任何联结词的谓词公式 子句：一些文字或其非的析取 子句集：所有子句的集合 计算过程 将谓词公式转化为前束合取