子句与子句集
Clause and clause set


为 使 用 归 结 方 法 ， 首 先 要 把 F1∧F2∧…∧Fn∧～ G 化成一种称作子句形的 标准形式。一般地，归结推理规则所应用的对 象是命题或谓词公式的一种特殊的形式，称为 子句(Clause) 一个子句就是一组文字的析取，一个文字或是 一个原子 ( 这时也称为正文字 ) ，或者是一个原 Q、 ~ R 都是 子的否定(这时也称为负文字)，如 P、 文字， P Q ~ R 是子句。

（2） C1 :~ P Q, C 2 : P C1 和 C2的归结式为 Q 。因为 C1 可以写作 P Q, 所以可以知道假言推理也是归结的一个特例。 （3） C1 :~ P Q R, C 2 :~ Q ~ R C1 和 C2 存在两个归结式，一个是 ~ P R ~ R 另一个是:~ P Q ~ Q 。 在这个例子中，只能是在 Q 上或 R 上进行归 结，不能两者同时进行归结，也就是说 ~ P 不 是归结式。
3.8.1 命题逻辑中的归结法 Resolution method in propositional logic


设有命题逻辑描述的命题F1，F2 ,…,Fn和G,要 求来证明在 F1∧F2∧…∧Fn 成立的条件下有 G 成立,或说F1∧F2∧…∧Fn G是定理(重言式)， 这就是我们的问题。如何建立推理规则，来 证明这个定理便是我们的任务。 很 显 然 F1∧F2∧…∧Fn G 是 重 言 式 等 价 于 F1∧F2∧…∧Fn∧～ B 是矛盾 ( 永假 ) 式。归结 推理方法就是从 F1∧F2∧…∧Fn∧～ B 出发， 使用归结推理规则来寻找矛盾，最后证明定 理 F1∧F2∧…∧FnG 的成立。这种方法可称作反演推理方法。
归结推理过程
Resolution reasoning proced Nhomakorabeare

从子句集 S 出发，仅只对 S 的子句间使用归结 推理规则，并将所得归结式仍放入 S 中，进而 再对新子句集使用归结推理规则，重复这些步 骤直到得到空子句□，便说明S是不可满足的， 从而与S对应的定理F1∧F2∧…∧Fn G是成 立的。 因为归结推理规则是正确的推理规则，归结式 是原两子句的逻辑推论，于是归结过程出现空 子句□，说明S中必有矛盾。
( P ~ R) (~ Q ~ R P)
一个子句的合取范式(CNF形式)常常表示为一个子
句的集合，即：
S {P ~ R, ~ Q ~ R P}
称为对应公式的子句集，其中每个元素都是一个子 句。把公式表示为子句集只是为了说明上的方便。
归结式 Resolvent


命题逻辑的归结规则可以陈述如下。 ' ' C2 C 1 P C 1 , C 2 ~ P C 2 设有两个子句: (其中 C1 、 是子句, P 是文字),从中消去互补对(即 P 和 ~ P ), ' ' C2 R ( C 1 , C 2 ) C 1 C 2，便称作子句 C1， 所得的新子句: 的归结式，原子P 称为被归结的原子。这个过 程称为归结。没有互补对的两个子句没有归结 式。 因此归结推理规则指的是对两个子句做归结， 即求归结式。上述归结规则是一种合理的推理 规则，这可从下述定理中看出。

（4）C1 :~ P Q, C 2 :~ P R C1中的任何文字都不能与 C2 中的文字构成互补 对，所以C1 和 C2 不存在归结式。 （5） C1 : Q, C 2 :~ Q Q 和~ Q是互补的，将它们分别由 C 和 C 中删除， 2 1 再构造 C1 和 C2其余部分的析取式，得出的归结 式是空子句 (Null clause) ，用□表示。这说明 由于 Q 和 ~ Q的互补性，它们不能同时成立。所 以空子句的出现代表出现了矛盾。
例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.2 子句 C1 和 C2 的归结式是 C1和C2 的逻辑推论。 证明：设
C1 P C1' , C 2 ~ P C 2'
有
R(C1, C 2) C1' C 2'
' C 1 其中 和 C 2 '都是文字的析取式。
Proof:
假定 C1 和 C2根据某种解释 I 为真。若 P 按 解释 I 为假，则 C1必不是单元子句(即单个文字), I C1 否则C1按I 解释为假。因此，按 ' ' R ( C 1 , C 2 ) C 1 C 2 必为真，即归结式 按 I 为真。 若P按I解释为真，则 ~ P按I为假，此时 C2 必不是单元子句，并且 C 2 '必按 I 为真，所以 R(C1, C 2) C1' C 2' 按I为真。由此得出，R(C1, C 2)是 C1 和 C2 的逻辑推论。定理得证

我们知道：对任意公式，都有与之等值的合取 范式，即对任意公式G 都有形如 G1 ... Gn(n 1) 的 公式与之等价，其中每个 Gi 都是文字的析取式， 就是一个子句。可以使用各种等价式将任意一 个公式 G 转化为一个合取范式。例如，可以把 公式 ~ ( P Q) ( R P) 转换为如下的合取范式:

例3.3 计算下述子句的归结式： （1） C1 : P R, C 2 :~ P Q 子句C1中的文字P和子句 C2 中~ P 的文字是互补的。 由 C1 和 C2 中分别删除 P 和~ P ,并且构造两个子句 的 其 余 部 分R 和 Q 的 析 取 式 ， 得 出 归 结 式 为 RQ 。 这两个被归结的子句可以写成： ~ R P, P Q,根据 假言三段论，可以推出~ R Q ,它等价于 R Q 。 因此可以知道假言三段论是归结的一个特例。