离散数学_第三章_消解原理.docVIP

*第三章 消 解 原 理 3.1 斯柯伦标准形 内容提要 我们约定，本章只讨论不含自由变元的谓词公式(也称语句,sentences)，所说前束范式均指前束合取范式。 全称量词的消去是简单的。因为约定只讨论语句，所以可将全称量词全部省去，把由此出现于公式中的“自由变元”均约定为全称量化的变元。例如A(x)实指(xA(x)。 存在量词的消去要复杂得多。考虑(xA(x)。 （1）当A(x)中除x外没有其它自由变元，那么，我们可以像在自然推理系统中所做那样，可引入A(e/x)，其中e为一新的个体常元，称e为斯柯伦（Skolem）常元，用A(e/x)代替(xA(x),但这次我们不把A(e/x)看作假设,详见下文。 （2）当A中除x外还有其它自由变元y1,…,yn，那么 (xA(x, y1,…,yn) 来自于(y1…(yn(xA(x, y1,…,yn)，其中“存在的x”本依赖于y1,…,yn的取值。因此简单地用A(e/x, y1,…,yn)代替 (xA(x, y1,…,yn) 是不适当的，应当反映出x对y1,…,yn的依赖关系。为此引入函数符号f，以A(f(y1,…,yn)/x, y1,…,yn) 代替 (xA(x, y1,…,yn)，它表示：对任意给定的y1,…,yn, 均可依对应关系f确定相应的x，使x, y1,…,yn满足A。这里f是一个未知的确定的函数，因而应当用一个推理中尚未使用过的新函数符号，称为斯柯伦函数。 定理3.1（斯柯伦定理）对任意只含自由变元x, y1,…,yn的公式A(x, y1,…,yn)，(xA(x, y1,…,yn)可满足，当且仅当A(f(y1,…,yn), y1,…,yn)可满足。这里f为一新函数符号；当n = 0时，f为新常元。 定义3.1 设公式A的前束范式为B。C是利用斯柯伦常元和斯柯伦函数消去B中量词（称斯柯伦化）后所得的合取范式，那么称C为A的斯柯伦标准形（Skolem normal form）。 以下我们约定：斯柯伦标准形中，各子句之间没有相同的变元。 定义3.2 子句集S称为是可满足的，如果存在一个个体域和一种解释，使S中的每一个子句均为真，或者使得S的每一个子句中至少有一个文字为真。否则, 称子句集S是不可满足的。 ? 习题解答 练习3.1 1、求下列各式的斯柯伦标准形和子句集。 （1）┐((xP(x)→(y(zQ(y, z)) （2）(x(┐E(x, 0)→(y(E(y, g(x))∧(z(E(z, g(x))→E(y, z)))) （3）┐((xP(x)→(y P(y)) （4） （1）∧（2）∧（3） 解（1）┐((xP(x)→(y(zQ(y, z))┝┥┐(xP(x)∧(y(zQ(y, z) ┝┥(x┐P(x)∧(y(zQ(y, z) 斯柯伦标准形：┐P(e1)∧Q(e2, z) 子句集：{┐P(e1)，Q(e2, z)} ? （2）(x(┐E(x, 0)→(y(E(y, g(x))∧(z(E(z, g(x))→E(y, z)))) ┝┥(x(y(z (E(x, 0)∨(E(y, g(x))∧(┐E(z, g(x))∨E(y, z)))) ┝┥(x(y(z ((E(x, 0)∨E(y, g(x)))∧(E(x, 0)∨┐E(z, g(x))∨E(y, z))) 斯柯伦标准形：(E(x, 0)∨E(f(x), g(x)))∧(E(x, 0)∨┐E(z, g(x))∨E(f(x), z)) 子句集：{ E(x, 0)∨E(f(x), g(x)), E(x, 0)∨┐E(z, g(x))∨E(f(x), z)} （3）┐((xP(x)→(y P(y))┝┥(xP(x)∧┐(y P(y) ┝┥(xP(x)∧(y┐P(y) ┝┥(x(y (P(x)∧┐P(y)) 斯柯伦标准形：P(x)∧┐P(y) 子句集：{P(x),┐P(y) } ? （4）（1）∧（2）∧（3） 斯柯伦标准形：┐P(e1)∧Q(e2, z)∧(E(x, 0)∨E(f(x), g(x)))∧(E(u, 0)∨┐E(y, g(u))∨E(f(u), y))∧P(w)∧┐P(v) 子句集：{┐P(e1)，Q(e2, z), E(x, 0)∨E(f(x), g(x)), E(u, 0)∨┐E(y, g(u))∨E(f(u), y), P(w),┐P(v)} ? 2、设公式A1，A2的子句集分别为S1，S2，如果S1与S2等值（表示对应的斯柯伦标准形有相等的真值）