-
基礎歸結
鎖定
- 中文名
- 基礎歸結
- 所屬學科
- 數學
- 相關概念
- 基礎子句集，原子公式，互補子等
- 所屬問題
- 歸結定理與歸結方法
基礎歸結基本介紹
相關概念
互補子如果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]
。
基礎歸結例題解析
例1 n階基礎歸結。
給定子句集
，有
例2 設：
，通過D賦值(半解釋)：
(1)求基礎歸結原始表達式
；
(2)證明
；
(3)證明S與
的不可滿足性是完全一致的(即S不可滿足
不可滿足)。
解答：
(1)根據定義(基礎歸結)，
。
(2)根據表1第3、4列，顯然有如果
，則
；如果
，則
，因此，
成立。
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 | ||||
