*第三章消解原理斯柯伦标准形内容提要我们约定，本章只讨论不含自由变元的谓词公式(也称语句,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,…,y n，那么xA(x, y1,…,y n) 来自于y1…y n xA(x, y1,…,y n)，其中“存在的x”本依赖于y1,…,y n的取值。
因此简单地用A(e/x, y1,…,y n)代替xA(x, y1,…,y n) 是不适当的，应当反映出x对y1,…,y n的依赖关系。
为此引入函数符号f，以A(f(y1,…,y n)/x, y1,…,y n) 代替xA(x, y1,…,y n)，它表示：对任意给定的y1,…,y n, 均可依对应关系f确定相应的x，使x, y1,…,y n满足A。
这里f是一个未知的确定的函数，因而应当用一个推理中尚未使用过的新函数符号，称为斯柯伦函数。
定理（斯柯伦定理）对任意只含自由变元x, y1,…,y n的公式A(x, y1,…,y n)，xA(x, y1,…,y n)可满足，当且仅当A(f(y1,…,y n), y1,…,y n)可满足。
这里f为一新函数符号；当n = 0时，f为新常元。
定义设公式A的前束范式为B。
C是利用斯柯伦常元和斯柯伦函数消去B中量词（称斯柯伦化）后所得的合取范式，那么称C为A的斯柯伦标准形（Skolem normal form）。
以下我们约定：斯柯伦标准形中，各子句之间没有相同的变元。
定义子句集S称为是可满足的，如果存在一个个体域和一种解释，使S中的每一个子句均为真，或者使得S的每一个子句中至少有一个文字为真。
否则, 称子句集S是不可满足的。
习题解答练习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等值（表示对应的斯柯伦标准形有相等的真值），问是否一定有A1与A2等值，为什么解 不一定有A1与A2等值。
例如，个体域为自然数集合，A1为y P(y)，A2为y Q(y)，P(y)表示：y 是偶数，Q(y)表示：y 是负数。
y P(y)与y Q(y)不等值，但P(e1)与Q(e2)在解释I 把e1，e2确定为奇数时，却是等值的。
3、假如要利用子句集不可满足性来证明(P →Q)∧(Q →R)→(P →R)永真。
试作出待证公式否定的子句集。
解 待证公式否定的子句集为：{ ┐P ∨Q, ┐Q ∨R,P, ┐Q}4、要利用子句集不可满足性来证明例的推理是正确的。
试作出这一推理的否定（┐（前提1∧前提2→结论））的子句集。
解5. 试简述A(e/x) 或A(f(y 1,…,y n )/x, y 1,…,y n ) 可以在应用消解原理的推理中代替 xA(x) 或 y 1…y n xA(x, y 1,…,y n ) 的原因,以及选择e,f 应注意的事项。
解 A(e/x) 或A(f(y 1,…,y n )/x, y 1,…,y n ) 可以在应用消解原理的推理中代替 xA(x) 或 y 1…y n xA(x, y 1,…,y n ) 的原因是：（1） （1）用消解原理证明定理A 或证明 ┝A ，是通过确认┐A 和B 1∧∧B n ∧┐A(B 1,,B n 为中公式)的不可满足性来实现的。
（2） （2）A(e/x) ，A(f(y 1,…,y n )/x, y 1,…,y n )与xA(x) ，y 1…y n xA(x,y 1,…,y n )的不可满足性是相同的。
选择e,f 应注意选择新常元和新函数符号，即在推理过程中尚未使用过的常元和函数符号。
命题演算消解原理内容提要关于命题演算的消解原理。
设C1，C2为两个子句，L1，L2是分别属于C1，C2的互补文字对，用C-L 表示从子句C 中删除文字L 后所得的子句，那么消解原理可表示为)22()11(2,1L C L C C C -∨- 其中C1,C2称为消解母式，L1，L2称为消解基，而(C1-L1)∨(C2-L2)称为消解结果。
特别地，当C1，C2都是单文字子句，且互补时，C1，C2的消解结果不含有任何文字，这时我们称其消解结果是“空子句”（nil ），常用符号 □ 表示之, 空子句□是永远无法被满足的。
关于消解原理我们有：定理 设C 是C1，C2的消解结果，那么C 是C1和C2的逻辑结果。
本定理的证明可仿以上对式（）的证明，请读者自行完成。
据本定理知，消解原理作为推理规则是适当的。
作为特别情况，p 与┐p 的消解结果是□，□实质上是p ∧┐p 的另一种表示形式,它们都是不可满足的，因而也满足定理的结论。
定义 设S 为一子句集，称C 是S 的消解结果，如果存在一个子句序列C 1，C 2 ，…,C n （= C ），使C i (i = 1,2, …,n) 或者是S 中子句，或者是C k ，C j (k,j < i) 的消解结果。
该序列称为是由S 导出的C 的消解序列。
当□是S 的消解结果时，称该序列为S 的一个否证（refutations ）。
定理 如果子句集S 有一个否证，那么S 是不可满足的。
习题解答练习1、 1、完成定理证明。
证 设C1，C2为两个子句，L1，L2是分别属于C1，C2的互补文字对，用C-L 表示从子句C 中删除文字L 后所得的子句，那么消解原理可表示为)22()11(2,1L C L C C C -∨- 设C1，C2分别为L1∨C1’，L2∨C2’ ; L1，L2为消解基， 即C1’=C1- L1 ，C2’= C2- L2。
由于L2 = ┐L1，那么（L1∨C1’）∧（L2∨C2’）┝（L1∨C1’）∧（┐L1∨C2’）┝ （L1∧C2’）∨（C1’∧┐L1）∨（C1’∧C2’）┝ C1’∨C2’于是我们有(L1∨C1’)∧(L2∨C2’)┝（C1- L1）∨（C2- L2）即C1∧C2┝（C1- L1）∨（C2- L2）。
这就是说，C1与C2的消解结果是C1和C2的 逻辑结果。
2、证明下列子句集是不可满足的。
（1）S = {p ∨q, ┐q ∨r, ┐p ∨q, ┐r}解（1）p ∨q（2）┐q ∨r（3）┐p ∨q（4）┐r（5）┐q 由（2）（4）消解得（6）p 由（1）（5）消解得（7）┐p 由（3）（5）消解得（8）□（2）S = {p ∨q, q ∨r, r ∨w, ┐r ∨┐p, ┐w ∨┐q, ┐q ∨┐r}解（1）p ∨q（2）q ∨r（3）r ∨w（4）┐r ∨┐p（5）┐w ∨┐q（6）┐q ∨┐r（7）┐r ∨q 由（1）（4）消解得（8）q 由（2）（7）消解得（9）┐w 由（5）（8）消解得（10）┐r 由（6）（8）消解得（11）r 由（3）（9）消解得（12）□ 由（10）（11）消解得3、用消解原理证明下列逻辑蕴涵式。
（1）(p ∨q)→r ┝ (p →r)∧(q →r)解 S = {┐p ∨r,┐q ∨r, p ∨q , p ∨┐r, q ∨┐r, ┐r}（1）┐p ∨r（2）┐q∨r（3）p∨q（4）p∨┐r（5）q∨┐r（6）┐r（7）┐p 由（1）（6）消解得（8）┐q 由（2）（6）消解得（9）q 由（3）（7）消解得（10）□由（8）（9）消解得（2）(p→r)∧(q→r) ┝ (p∨q)→r解S = {┐p∨r,┐q∨r, p∨q , ┐r}（1）┐p∨r（2）┐q∨r（3）p∨q（4）┐r（5）┐p 由（1）（4）消解得（6）┐q 由（2）（4）消解得（7）q 由（3）（5）消解得（8）□由（6）（7）消解得（3）(p→(┐q∨(r∧s)))∧p∧┐s┝┐q解S = {┐p∨┐q∨r, ┐p∨┐q∨s, p,┐s, q }（1）┐p∨┐q∨r（2）┐p∨┐q∨s（3）p（4）┐s（5）q（6）┐q∨s 由（2）（3）消解得（7）s 由（5）（6）消解得（8）□由（4）（7）消解得（4）(p∨q)∧(p→r)∧(q→s) ┝ r∨s解S = { p∨q,┐p∨r, ┐q∨s, ┐r,┐s }（1）p∨q（2）┐p∨r（3）┐q∨s（4）┐r（5）┐s（6）┐q 由（3）（5）消解得（7）p 由（1）（6）消解得（8）r 由（2）（7）消解得（9）□由（4）（8）消解得4、已知有如下化学反应方程式MgO+H2→Mg+H2OC+O2→CO2CO2+H2O→H2CO3现假定有物质MgO，H2，O2和C，形式证明可生成H2CO3。
