离散数学导论(盘) 作者 王元元 张桂芸 第三章演示文稿.pptVIP

* * 第 三 章 消 解 原 理 在线教务辅导网： 教材其余课件及动画素材请查阅在线教务辅导网 QQ:349134187 或者直接输入下面地址： 3.1 斯柯伦标准形 3.2 命题演算消解原理 3.3 谓词演算消解原理 *第三章 消 解 原 理 3.1.1 斯柯伦标准形 3.1.2 子句集及其可满足性 *第三章 消 解 原 理 3.1 斯柯伦标准形 3.3.1 代换及一致化 3.3.2 谓词演算消解原理 *第三章 消 解 原 理 3.3 谓词演算消解原理 *第三章 消 解 原 理 3.1 斯柯伦标准形 3.1.1 斯柯伦标准形 对任意只含自由变元x, y1,…,yn的公式 A(x, y1,…,yn)，?xA(x, y1,…,yn)可满足， 当且仅当A(f(y1,…,yn), y1,…,yn)可满足。 这里f为一新函数符号；当n=0时，f 为 新常元。 定理3.1 （斯柯伦定理） *第三章 消 解 原 理 3.1 斯柯伦标准形 3.1.1 斯柯伦标准形 设公式A的前束范式为B。C是利用 斯柯伦常元和斯柯伦函数消去B中量词 （称斯柯伦化）后所得的合取范式，那么称 C为A的斯柯伦标准形 （Skolem normal form）。 定义3.1 *第三章 消 解 原 理 3.1 斯柯伦标准形 3.1.2 子句集及其可满足性 定义3.2 子句集S称为可满足的，如果存在一个 个体域和一种解释，使S中的每一个子 句均为真，或使得S中的每一个子句 至少有一个文字为真。否则称S为不可满足的。 *第三章 消 解 原 理 3.2 命题演算消解原理 设C是C1，C2的消解结果，那么 C是C1和C2的逻辑结果。 定理3.2 *第三章 消 解 原 理 3.2 命题演算消解原理 设S为一子句集，称C是S的消解结果， 如果存在一个子句序列C1，C2 ，…,Cn（=C）， 使Ci(i=1,2, …,n)或者是S中子句，或者是 Ck，Cj (k,j i)的消解结果。该序列称为由S 导出的C的消解序列。当□是S的消解结果时， 称该序列为S的一个否证（refutation）。 定义3.3 *第三章 消 解 原 理 3.2 命题演算消解原理 如果子句集S有一个否证， 那么S是不可满足的。 定理3.3 *第三章 消 解 原 理 3.3 谓词演算消解原理 3.3.1 代换及一致化 形如{t1/v1, t2/v2, …, tn/vn}的有穷集合称为一个代换 （substitution），其中v1,…, vn为任意变元，t1,…,tn为 任意个体项，但ti≠vi(i=1,2, …,n)。当代换为一空集合 时，称为空代换。代换用小写希腊字母表示，空代换 记为?，“对任意公式或项X作代换?”记为X?，其意 为对X中变元v1,v2,…, vn分别作代入t1,…,tn，即 X?= X(t1/v1, t2/v2, …, tn/vn) 对于空代换?有X?= X。 定义3.4 *第三章 消 解 原 理 3.3 谓词演算消解原理 3.3.1 代换及一致化 设?={t1/x1,…,tn/xn}, ? ={s1/y1,…,sm/ym}是两个代换，?与?的合成，记为???，指如下所得的代换： 从{ t1?/x1,…,tn?/xn, s1/y1,…,sm/ym }中删去 （1）si/yi，当yi恰为x1,…,xn之一 （2）ti?/xi，当ti?=xi。 定义3.5 *