*第三章 消 解 原 理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...
