來自 中国最大的资料库下载
3.2.3 Resolution Refutations（2）
• 归结方法是一种机械化的,可在计算机上加以实现 的推理方法
• 可认为是一种反向推理形式 • 提供了一种自动定理证明的方法
3.2.3 Resolution Refutations（3）
• 一般过程:
3.2.4 Soundness and Completeness
• 归结原理是合理的 • 归结原理是完备的
– Convert to CNF by using the associative an distributive laws.
3.2.2 Resolution
• 对任意三个子句 p、q 和 r p r, q ~r p q
或者： for C1= P C1’, C2=~P C2’ P C1’, ~P C2’ C1’ C2’
• 归结法的本质上就是一种反证法，它是在归结推理规则的 基础上实现的：
为了证明一个命题P恒真，它证明其反命题～P恒假，即不 存在使得P为真的解释
ห้องสมุดไป่ตู้
3.2 命题逻辑中的归结原理
3.2.1 子句和子句形 3.2.2 归结 3.2.3 归结反演 3.2.4 合理性和完备性 3.2.5 归结反演的搜索策略
3.2.1 子句和子句形（1）
人工智能原理课件
2020/8/7
3.1 Introduction
• 证明的基本思想是： 设F1、…、Fn、G为公式，G为F1、…、Fn的逻辑推论，当 仅当公式（（F1…Fn）G）是有效的
• 也可以采用反证法的思想： 设F1、…、Fn、G为公式，G为F1、…、Fn的逻辑推论，当 仅当公式（F1…Fn G）是不可满足的
• 归结式： R(C1, C2)=C1’ C2’ • 证明：
3.2.3 Resolution Refutations（1）
• 定理证明的任务: 由前提A1 A2 ... An 推出结论B 即证明:A1 A2 ... AnB 永真
• 转化为证明: A1 A2 ... An ~B为永假式
• 归结推理就是:从A1 A2 ... An ~B出发,使 用归结推理规则来找出矛盾,最后证明定理A1 A2 ... AnB的成立
1) 建立子句集S 2) 从子句集S出发,仅对S的子句间使用归结推理规则 3) 如果得出空子句•, 则结束;否则转下一步 4) 将所得归结式仍放入S中 5) 对新的子句集使用归结推理规则 6) 转(3) • 空子句不含有文字,它不能被任何解释满足,所以空子句是永 假的,不可满足的
• 归结过程出现空子句,说明出现互补子句对,说明S中有矛盾 因此S是不可满足的.
• 文字是原子或其否定 • 子句是文字的析取 • 完备连接符集合： • 合取范式（CNF）
（L11 … L1n1) … (Lm1 … Lmnm) • 析取范式（DNF）
（L11 … L1n1) … (Lm1 … Lmnm)
• 定理： 对任意公式，都有与之等值的合取范式和析取范式
• 转换方法：一般方法 真值表方法
3.2.3 Resolution Refutations（4）
• 例子:证明(P Q) ~Q ~p • 首先建立子句集:
– (P Q)~Q ~(~P) – (~P Q) ~Q P – S={~PQ, ~Q , P} • 对S作归结:
(1) ~P Q (2) ~ Q (3) P (4) ~P (1)(2)归结 (5) • (3)(4)归结
3.2.2子句和子句形（2）
• 一般方法
– Eliminate implication signs by using the equivalent form using
– Reduce the scopes of ~ signs by using DeMorgan’s law and by eliminating double signs