应的所有变量，并且去掉第一个存在量词而得出 的公式,(k=1,…,m),显然 S Gm。与上面的证明相似， 可以证明 Gk1 是不可满足的，当且仅当 Gk 是不可 满足的(k=1,…,m)。所以可以断定， G 是不可满 足的，当且仅当S 是不可满足的。
例3.6 G (x)P(x)的SKOLEM标准形与 G并不是等值 的。
（1）C1: P R,C2 :~ P Q
子句C1中的文字P和子句 C2中~ P 的文字是互补的。 由 C1和 C2 中分别删除 P和~ P,并且构造两个子句 的 其 余 部 分R 和 Q的 析 取 式 ， 得 出 归 结 式 为 RQ 。
这两个被归结的子句可以写成：~ R P, P Q,根据 假言三段论，可以推出~ R Q,它等价于 R Q 。 因此可以知道假言三段论是归结的一个特例。
真,只要在论域D中能找到一个个体x 0使 P( x0)为真。而
G1 =P(a) 是 从 论 域 中 选 定 一 个 个 体 a ， 这 样 不 能 保 证 P(a)为真。
例3.7 G (x)(y)P(x, y)
G1 (x)P(x, f (x))
考虑G 与G1 的逻辑关系。 仍在论域D={1,2}上讨论。便有
子句型
Clause form
归结证明过程是一种反驳程序，即：不是证明一 个公式是有效的(valid)，而是证明公式之非是不 可 满 足 的 (unsatisfiable)。 这 完 全 是 为 了 方 便 ， 并且不失一般性。我们知道，归结推理规则所应 用的对象是命题或谓词合式公式的一种特殊的形 式，称为子句。因此在进行归结之前需要把合式 公式化为子句式。
很F推1∧理显F方然2∧法F…1就∧∧F是F2∧从n∧…F～1∧∧BFF是n2∧矛…盾G 是∧(永F重n∧假言～)式式B等出。价归发
于 结 ，
使用归结推理规则来寻找矛盾，最后证明定
理
F1∧F2∧…∧Fn G
的成立。这种方法可称作反演推理方法。
子句与子句集
Clause and clause set
为 使 用 归 结 方 法 ， 首 先 要 把 F标1∧准F形2∧式…。∧一F般n∧地～，G归化结成推一理种规称则作所子应句用形的的对 象是命题或谓词公式的一种特殊的形式，称为 子句(Clause)
例3.4 证明 (P Q) ~ Q ~ P 先将 (P Q) ~ Q ~ (~ P)
化成合取范式，得 (~ P Q) ~ Q P
建立子句集
S {~ P Q, ~ Q, P}
对S做归结
(1) ~ P Q
(2) ~ Q
(3) P (4) ~ P （1）（2）归结 (5) □ （3）（4）归结 证毕。
3.8.1 命题逻辑中的归结法
Resolution method in propositional logic
设求成这立有来就,命证是或题明我说逻在们F1辑的F∧1∧描问F2F述∧题2∧的…。…命∧如∧题F何nFF建n1成，G立是F立推2定的,…理理条,规F(件重n则和下言，G有,式要来G)，
证明这个定理便是我们的任务。
归结推理过程
Resolution reasoning procedure
从子句集S出发，仅只对S的子句间使用归结 推理规则，并将所得归结式仍放入S中，进而 再对新子句集使用归结推理规则，重复这些步 骤直到得到空子句□，便说明S是不可满足的，
从而与S对应的定理F1∧F2∧…∧Fn G是成
立的。
因为归结推理规则是正确的推理规则，归结式 是原两子句的逻辑推论，于是归结过程出现空 子句□，说明S中必有矛盾。
3.8.2 谓词逻辑中的归结法
Resolution method in predicate logic
和命题逻辑一样，在谓词逻辑中也具有归 结推理规则和归结反演过程。只是由于谓词 逻辑中存在量词、个体变元等问题，使得谓 词逻辑中的归结问题比命题逻辑中的归结问 题复杂很多。下面就来介绍谓词逻辑中的归 结法。
（2） C1:~ P Q,C2 : P
C1和 C2的归结式为 Q 。因为 C1可以写作 P Q, 所以可以知道假言推理也是归结的一个特例。
（3） C1:~ P Q R,C2 :~ Q ~ R
C1和 C2 存在两个归结式，一个是 ~ P R ~ R
另一个是:~ P Q ~ Q。
在这个例子中，只能是在 Q 上或 R 上进行归 结，不能两者同时进行归结，也就是说 ~ P 不 是归结式。
一个子句就是一组文字的析取，一个文字或是 一个原子(这时也称为正文字)，或者是一个原 子的否定(这时也称为负文字)，如 P、Q、~ R 都是 文字， P Q ~ R 是子句。
我们知道：对任意公式，都有与之等值的合取 范式，即对任意公式G 都有形如G1...Gn(n 1) 的 公式与之等价，其中每个 Gi 都是文字的析取式， 就是一个子句。可以使用各种等价式将任意一 个公式G转化为一个合取范式。例如，可以把 公式 ~ (P Q) (R P) 转换为如下的合取范式:
(Qr 1xr 1)...(Qnxn)M (x1,..., xr 1, f (x1,..., xr 1), xr 1,..., xn)
按I1为真。即G1 | I1 T，这与G1是不可满足的假设 相矛盾。所以G 必是不可满足的。
假设G中有m个存在量词。令 G0 G，设 Gk 是在 Gk1中用Skolem函数代替其中第一个存在量词所对
在第3.1节中已经介绍了如何把一个公式化成前 束标准型(Q1x1)...(Qnxn)M ,由于M中不含量词总可以 把它变换成合取范式。无论是前束标准型还是合 取范式都是与原来的合式公式等值的。
Skolem标准化过程
Step1: 化成前束范式: (Q1x1)...(Qnxn)M (x1,..., xn)
按上述方法删去前缀中的所有存在量词之后得出的公式称 为合式公式的Skolem标准型。替代存在量化变量的常量c(视 为0元函数)和函数f称为Skolem函数。
例3.5 化公式
xyzuvwP(x, y, z,u,v, w)
为Skolem标准型。
在公式中， x的前面没有全称量词，在u的前
面有全称量词(y) 和(z) ,在 (w) 的前面有全称量 词(y) ，(z)和 (v)。所以，在P(x, y, z,u,v, w) 中，用常 数 a 代 替 x, 用 二 元 函 数 f(y,z) 代 替 u, 用 三 元 函 数 g(y,z,v)代替w,去掉前缀中的所有存在量词之后 得出Skolem标准型：
设 (Qrxr为) 前缀中的第一个存在量词。令
G1 (x1)...(xr 1)(Qr 1xr 1)(Qnxn)M (x1,..., xr 1, f (x1,..., xr 1), xr 1,..., xn)
其中，f (x1,..., xr 1)是对应 xr的Skolem函数。我们希
望证明 G是不可满足的，当且仅当 G1 是不可满足 的。
(Qr 1xr 1)...(Qnxn)M (x1,..., xr 1, xr, xr 1,..., xn)
按I为真。扩充解释I，使得包括对任意x1 D,..., xr 1 D 把(x1,..., xr 1)映射成 xr D的函数f，即
f (x1,..., xr 1) xr
扩充后的解释用I1表示。显然，对任意x1 D,..., xr 1 D
Step2: 使用下述方法可以消去前缀中存在的所有量词 令Qr是 (Q1x1)...(Qnxn) 中出现的存在量词(1 r n) .
Case1:若在Qr之前不出现全称量词，则作置换: {c/xr }，c是一个 与M中出现的所有常量都不相同的新常量c，用c代替M中出现 的所有xr，并且由前缀中删去 Qr 。 Case2:若在Qr之前出现全称量词Qs1,...,Qsm ，则选择一个与M中 出现的任一函数符号都不相同的新m元函数符号f，用f (xs1,..., xsm) 代替M中的所有xr ，并且由前缀中删去Qr 。
设G 是不可满足的。若G1 是可满足的，则存在 某定义域D上的解释I使 G1 按I为真。即对任意
x1 D,..., xr 1 D
(Qr 1xr 1)...(Qnxn)M (x1,..., xr 1, f (x1,..., xr 1), xr 1,..., xn)
按I为真，所以，对任意 x1 D,..., xr 1 D ，都存在 元素 f (x1,..., xr 1) xr D 使
是子句, P是文字),从中消去互补对(即P 和 ~ P ),
所得的新子句:
R(C1,
C
2)
C
' 1
C
'
2，便称作子句C1，C2
的归结式，原子P 称为被归结的原子。这个过
程称为归结。没有互补对的两个子句没有归结 式。
因此归结推理规则指的是对两个子句做归结， 即求归结式。上述归结规则是一种合理的推理 规则，这可从下述定理中看出。
(P ~ R) (~ Q ~ R P)
一个子句的合取范式(CNF形式)常常表示为一个子 句的集合，即：
S {P ~ R, ~ Q ~ R P}
称为对应公式的子句集，其中每个元素都是一个子 句。把公式表示为子句集只是为了说明上的方便。
归结式
Resolvent
命题逻辑的归结规则可以陈述如下。
设有两个子句: C1 P C'1,C2 ~ P C' 2 (其中 C1 、C2
定理3.2 子句 C1 和 C2 的归结式是C1和C2的逻辑推论。 证明：设
C1
P
C1'
,
C
2
~
P
C
' 2
ห้องสมุดไป่ตู้
有
R(C1,
C
2)
C1'
C
' 2
其中C1' 和 C2'都是文字的析取式。