歸結

歸結原理是1965年美國人Robinson提出的一種證明一階謂詞演算中定理的方法。使用這種方法時，對任一要證明的永真公式取非後，證明它不可滿足，為此先轉化成一種標準型，然後對這個標準型不斷使用單一的推理規則，即實行歸結，直到導出矛盾。

基本介紹

• 中文名：歸結
• 提出人：Robinson
• 時間：1965
• 運用：證明一階謂詞演算中定理

簡介

由謂詞公式轉化子句集的過程可以了解到：子句集中的子句之間是合取關係，其中只要有一個子句不可滿足，則子句集就不可滿足。另外，空子句是不可滿足的。因此，若一個子句集中包含空子句，則這個子句集一定是不可滿足的。Robinson歸結原理就是基於這一認識提出來的。其基本思想是：檢查子句集S中是否包含空子句，若包含，則S不可滿足；若不包含，就在子句集中選擇合適的子句進行歸結，一旦通過歸結能推出空子句，就說明子句集S是不可滿足的。

命題邏輯中的歸結原理

定義1

若P是原子謂詞公式，則稱P與¬P為互補文字。

定義2

設C₁與C₂是子句集中的任意兩個子句，如果C₁中的文字L₁與C₂中的文字L₂互補，那么從C₁和C₂中分別消去L₁和L₂，並將兩個子句中餘下的部分析取，構成一個新子句C₁₂，則稱這一過程為歸結，稱C₁₂為C₁和C₂的歸結式，稱C₁和C₁為C₁₂的親本子句。

定理1

歸結式C₁₂是其親本子句C₁與C₂的邏輯結論。

這個定理是歸結原理中的一個很重要的定理，由它可得到如下兩個推論：

推論1

設C₁與C₂是子句集S中的兩個子句，C₁₂是它們的歸結式，若用C₁₂代替C₁和C₂後得到新子句集S₁，則由S₁的不可滿足性可推出原子句集S的不可滿足性，即：S₁的不可滿足性⇒S的不可滿足性

推論2

設C₁與C₂是子句集S中的兩個子句，C₁₂是它們的歸結式，若把C₁₂加入S中，得到新子句集S₂，則S與S₂在不可滿足的意義上是等價的，即：S₂的不可滿足性<=>S的不可滿足性

這兩個推論給出了用歸結原理證明子句集不可滿足性的基本思想：為了要證明子句集S的不可滿足性，只要對其中可進行歸結的子句進行歸結，並把歸結式加入子句集S，或者用歸結式替換它的親本子句，然後對新子句集（S₁或S₂）證明不可滿足性就可以了。如果經過歸結能得到空子句，根據空子句的不可滿足性，可得出原子句集S是不可滿足的。

在命題邏輯中，對不可滿足的子句集S，歸結原理是完備的，即：若子句集不可滿足，則必然存在一個從S到空子句的歸結演繹；若存在一個從S到空子句的歸結演繹，則S一定是不可滿足的。但是，對於可滿足的子句集S，用歸結原理得不到任何結果。

謂詞邏輯中的

歸結原理

在謂詞邏輯中，由於子句中含有變元，所以不可直接消去互補文字，而需要先用最一般合一對變元進行代換，然後才能進行歸結。例如，設如下兩個子句：

C₁=P(x)∨Q(x)

C₂=¬P(A)∨R(y)

由於P(x)與P(A)不同，所以C₁與C₂不能直接進行歸結，但若用最一般合一

σ={A/x}

對兩個子句分別進行代換：

C₁σ=P(A)∨Q(A)，　C₂σ=¬P(A)∨R(y)

就可對它們進行歸結，消去P(A)與¬P(A)，得到如下歸結式：

Q(A)∨R(y)

下面給出謂詞邏輯中關於歸結的定義。

定義1：設C₁與C₂是兩個沒有相同變元的子句，L₁和L2分別是C₁和C₂中的文字，若σ是L₁和¬L2的最一般合一，則稱

C₁₂=（C₁σ－{L₁σ}）∪（C₂σ－{L₂σ}）

為C₁和C₂的二元歸結式，L₁和L2稱為歸結式的文字。

一般來說，若子句C中有兩個或兩個以上的文字具有最一般合一σ，則稱為Cσ為子句C的因子。如果Cσ是一個單文字，則稱它為C的單元因子。

套用因子的概念，可對謂詞邏輯中的歸結原理給出如下定義。

定義2：子句C₁和C₂的歸結式是下列二元歸結式之一：

①C₁與C₂的二元歸結式；

②C₁與C₂的因子C₂σ₂的二元歸結式；

③C₁的因子C₁σ₁與C₂的二元歸結式；

④C₁的因子C₁σ₁與C₂的因子C₂σ₂的二元歸結式。

對於謂詞邏輯，定理1仍然適用，即歸結式是它的親本子句的邏輯結論。用歸結式取代它在子句集S中的親本子句所得到的新子句仍然保持著原子句集S的不可滿足性。

另外，對於一階謂詞邏輯，從不可滿足的意義上說，歸結原理也是完備的，即：若子句集是不可滿足的，則必存在一個從該子句集到空子句的歸結演繹；若從子句集存在一個到空子句的演繹，則該子句集是不可滿足的。