* 第 三 章 消 解 原 理,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,形如t1/v1, t2/v2, , tn/vn的有穷集合称为一个代换 （substitution），其中v1, vn为任意变元，t1,tn为 任意个体项，但tivi(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,*第三章 消 解 原 理,3.3 谓词演算消解原理,3.3.1 代换及一致化,代换 称为表达式集合X1 , , Xn的一致化 （unifier），如果使 X1 = = Xn 。,定义3.6,*第三章 消 解 原 理,3.3 谓词演算消解原理,3.3.2 谓词演算消解原理,消解原理,这一过程表示：先对C1，C2作代换，使L1与 L2 （或 L1和L2）一致化，然后再消解掉L1和L2， 其余文字的析取便是C1，C2的消解结果。,