互补子

　　不含有任何连接词的谓词公式叫原子公式，简称原子。如果A是一个原子公式，那么，A和¬A互为对方的互补子，二者的关系称为互补，互补关系以“□”表示。

　　定义

　　如果A是一个原子公式，那么，A和互为对方的互补子，二者的关系称为互补，互补关系以“”表示1。

　　相关概念

　　模型不包含互补对的基础文字的一个集合称为一个模型。令M是一个模型，S是一个基础子句的集合，如果对于S中的所有元素C都包括M的元素，那么，M是S的模型。一般地，如果H是S中的Herbrand域，那么，仅当M是H(S)的模型。

　　基础归结原始表达式如果C和D是两个基础子句集，并且构成互补对集合，那么，基础子句集称为C和D的基础归结原始表达式。

　　注：此定义是说，归结的过程是在被赋值(半解释)的子句中剔除(处于或关系中的)互补原子的过程。剔除互补原子后的子句集即基础归结原始表达式。

　　基础归结 基础子句集S的元素以及S的所有基础归结原始表达式构成的集合称为基础归结，以表示。

　　n阶基础归结如果S是一个基础子句的集合，那么以表示S的n阶基础归结，它定义为：对于任何。

　　相关定理

　　定理1(Robinson第一定理)如果S是任意一个基础子句的集合，那么，S是不可满足的，当且仅当n≥0时，包含。

　　充分性证明：如果包含，即包含至少一个互补对，在这种情况下，S不可能包含一个模型从由于S不包含一个模型M，因此S是不可满足的。

　　必要性证明：只要证明，S如果不包含，那么就可以满足。令是所有中的原子公式，或者它们的互补子在中。令M是一个模型，定义如下：对于，是空集，即集合，或。当从0逐步增大，这表示M将中的子句中的原子公式逐步扩展到M之中，即不包含，由于无矛盾的子句，即存在S为真的解释，即S可满足。

　　定理2(Robinson第二定理)如果S是任意一个有穷子句的集合，那么，S是不可满足的，当且仅当存在有穷个S的H化基例集H(S)，包含。

　　证明：

　　根据Herbrand定理，S是不可满足当且仅当存在有限的不可满足的基例集H(S)；根据Robinson第一定理，对于基础子句集S，包含；而H(S)属于基础子句，所以包含。

　　综上所述，给定一阶命题G，在H上的基例集是H(S)，则

　　是归结方法。这是归结证明方法的定义。

　　由此可见，归结方法是一个综合性的证明方法，这是因为它经过以下若干步骤，对于被证命题G：

　　求其否定命题：

　　求的Skolem标准型，消除量词；

　　求的子句集S；

　　求子句集S的D域；

　　求子句集S的H域；

　　求基例集H(S)；

　　求原子集A；

　　求S的D解释；

　　求S的H解释；

　　判定H(S)不可满足性；

　　删除子句文字中的互补句，验证H(S)可满足性。

　　这个过程是原理层面的揭示，不是操作层面的步骤。一般而言，在归结操作层面，可不验证H(S)的不可满足性，而直接进行互补子句的消除，即进行子句的归结，从而验证子句的不可满足性。

　　归结方法虽然是通用的证明方法，但是它可以通过推理机实现(如Prolog)，因此一般作为人工智能的典型应用，即把它作为一种自动化的证明方法。但是，不通过自动证明也是可以完成的，因此它是一个独立的证明方法，而不是机器证明的专有方法。

　　例题解析

　　例1n阶基础归结。

　　给定子句集，有

　　例2设：，通过D赋值(半解释)：

　　(1)求基础归结原始表达式；

　　(2)证明；

　　(3)证明S与的不可满足性是完全一致的(即S不可满足不可满足)。

　　解答：

　　(1)根据定义(基础归结)，。

　　(2)根据表1第3、4列，显然有如果，则；如果，则，因此，成立。

　　(3)根据表1，第4列S和第5列R(S)的值完全一致，即S不可满足不可满足，S可满足可满足1。

1						2		3	4	5
赋值						S的子句		基础归结原始表达式	S(合取)	(归结)
	1	J	1	K	1	1	1	1	1	1
	1				0	1	0	1	0	0
	1		0	K	1	1	1	1	1	1
	1				0	1	0	0	0	0
	0	J	1	K	1	1	1	1	1	1
	0				0	1	0	1	0	0
	0		0	K	1	0	1	1	0	0
	0				0	0	0	0	0	0

　　本词条内容贡献者为:

　　胡建平 - 副教授 - 西北工业大学