如果C和D是兩個基礎子句集，並且L⊆C，M⊆D構成互補對集合，那么，基礎子句集r=r(C,D)=(C-L)∪(D-M)稱為C和D的基礎歸結原始表達式。基礎子句集S的元素以及S的所有基礎歸結原始表達式構成的集合稱為基礎歸結，以R(S)=S∪{r}表示。如果S是一個基礎子句的集合，那么以Rn(S)表示S的n階基礎歸結，它定義為：對於任何n≥0，R0(S)=S,Rn+1(S)=R(Rn(S)) 。
基本介紹
- 中文名：基礎歸結
- 所屬學科：數學
- 相關概念：基礎子句集，原子公式，互補子等
- 所屬問題：歸結定理與歸結方法
基本介紹,相關概念,基礎歸結的定義,相關定理,例題解析,
基本介紹
相關概念
互補子如果A是一個原子公式，那么，A和
互為對方的互補子，二者的關係稱為互補，互補關係以“
”表示。
模型 不包含互補對的基礎文字的一個集合稱為一個模型。令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)，因此一般作為人工智慧的典型套用，即把它作為一種自動化的證明方法。但是，不通過自動證明也是可以完成的，因此它是一個獨立的證明方法，而不是機器證明的專有方法。
例題解析
例1 n階基礎歸結。
給定子句集
，有
例2 設：
，通過D賦值(半解釋)：
(1)求基礎歸結原始表達式
；
(2)證明
；
(3)證明S與
的不可滿足性是完全一致的(即S不可滿足
不可滿足)。
解答：
(1)根據定義(基礎歸結)，
。
(2)根據表1第3、4列，顯然有如果
，則
；如果
，則
，因此， 成立。
(3)根據表1，第4列S和第5列R(S)的值完全一致，即S不可滿足 不可滿足，S可滿足 可滿足。
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 | ||||
