第 4 讲 归结原理(不讲)课件.ppt

人工智能原理第 四 讲 归结原理;归结原理; 4.1 引言;自动定理证明;1930年，Herbrand定理。 半可判定问题。 一阶逻辑的判定问题。 在一阶逻辑中，有没有方法可以判断任何一个命题是否定理？(有没有方法可以判断任何一个公式能不能从公理及推理规则推导出来)。 数理逻辑的基本问题。 1936年，证明基本问题是不可解的。 在一阶逻辑中，如果一个定理是正确的，则有一个机械的方法在有限步内证明它。 一阶谓词逻辑有很强的表达能力，凡可计算的函数就可由一阶谓词表达。 ;历史;王浩 1958年，IBM704电脑，3-5分钟，证明了《数学原理》中有关命题演算的全部220条定理。 1959年，8.4分钟，证明了《数学原理》中全部（350条以上）定理。 罗素：“我真希望，在怀特海和我浪费了10年的时间用手算来证明这些定理之前，就知道有这种可能。” 1983年获得首届自动定理证明???程碑奖。;四色定理;四色定理;三类方法;基于归结的方法;;类人的方法(human simulation);判定方法;吴方法; 4.2 一阶逻辑;一. 基本概念;1. 函数;2. 符号;3. 项;二. 合适公式(wff, well-formed formula);1. 举例;2. 约束变量与自由变量;3. 变量改名;定义(原子)： 如果P是n元谓词，t1，t2，... ，tn是项，则 P（t1，t2，... ，tn）是一个原子。 ;5. 合适公式（Wff);6. 五个联结符;7. 举例;三. 一阶谓词逻辑的公式解释;1. 对D域内计算公式的规则;2. 真值表;3. 联结符的一些重要性质;例1; ;例2;;;;4. 一些定义;例1;例2;四. 前束范式;1. 公式的等价;;;证明： 设(?x)G(x) ? (?x)H(x)=T (?x)G(x)=T，(?x)H(x)=T 对任一个e?D，G(x)=T并且H(x)=T 对任一个e?D，G(x)=T? H(x)=T 设(?x)G(x) ? (?x)H(x)=F 对任一解释，(?x)G(x)=F或者(?x)H(x)=F 设(?x)G(x)=F 存在e?D，G(e)=F G(e) ? H(e)=F;注意：;证明(?x)G(x) ? (?x)H(x) ? (?x)(G(x) ? H(x)) (?x)G(x) ? (?x)H(x) = T, 则(?x)(G(x) ? H(x))=T 设(?x)G(x) ? (?x)H(x)=F (?x)G(x)=F 且 (?x)H(x)=F 存在a?D，使G(a)=F。存在b?D，使H(b)=F.。 反例： 对任意e?D，e?a，G(e)=T。 对任意e?D，e?b，H(e)=T。 a?b 对任意e?D，G(e) ? H(e)=T。 (?x)(G(x) ? H(x))=T。 ;2. 化公式为前束范式步骤;;例1;例2;五. 合取范式与析取范式;1. 变换公式;;2. 化公式为合取范式(析取范式);例子:;六. 逻辑结论;定理1;(F1∧F2∧…∧Fn)→G = ~F1∨~F2∨…∨~Fn∨G 设G是公式F1，F2，… ，Fn的逻辑结论 要证：(~F1∨~F2∨…∨~Fn∨G)是永真式 F1，F2，…，Fn均为真 F1，F2，…，Fn中至少有一个为假 设公式(F1∧F2∧…∧Fn)→G为永真式 要证：G是公式F1，F2，… ，Fn的逻辑结论 要证：当F1，F2，…，Fn为真，G为真 (~F1∨~F2∨…∨~Fn∨G)是永真式 ;定理2;定理的定义; 4.3 子句形;一. SKOLEM 标准形;二. 化SKOLEM 标准形的方法; 例1; 例2;三. 子句与子句集; 子句集; 定理;;要证明定理: (A1?A2?A3?A4)?B 证明: (A1?A2?A3?A4?~B)是永假式; 证明: (A1?A2?A3?A4?~B)的子句集不相容; 根据推论, 只要分别求出A1, A2, A3, A4, ~B的子句集;;;;Skolem范式 Herbrand域 语义树 Herbrand定理 Davis的工作;动机;一阶逻辑下验证定理是困难的: 个体变量论城D的任意性. D中元素的任意性. 解释的个数的无限性. 是否能找到一个比较简单的、特殊的论域，使得只要在这个论域上该公式是不可满足的，便能保证该公式在任一论域上也是不可满足的? ——Herbrand域(简称H域)就具有这样的性质。 ; 一、 Herbrand域（H域）;例1;例2;例3; 二、基本概念;原子集（ Herbrand 基，H基）;例子;基础实例（基例）;注意; 三、Herbran