歸結反演

歸結反演亦稱消解反演，是一種證明定理的計算機過程。所使用的證明方法與數學中的反證法思想十分相似，歸結反演除了可用於定理證明外，還可用來求取問題的答案。

基本介紹

• 中文名：歸結反演
• 定義：用歸結原理證明結論為真的過程
• 套用：證明定理、求解問題
• 改進策略：刪除策略、限制策略

歸結反演的定義

套用歸結原理證明結論為真的過程稱為歸結反演。

設F為已知前提的公式集，Q為目標公式（結論），用歸結反演證明Q為真的步驟是：

① 否定Q，得到¬Q；

② 把¬Q併入到公式集F中，得到{F，¬Q}；

③ 把公式集{F，¬Q}化為子句集S；

④ 套用歸結原理對子句集S中的子句進行歸結，並把每次歸結得到的歸結式都併入S中。如此反覆進行，若出現了空子句，則停止歸結，此時就證明了Q為真。

基於歸結反演的問題求解

歸結反演除了可用於定理證明外，還可用來求取問題的答案，問題求解的方法與定理證明類似。問題求解的步驟如下：

① 把已知前提用謂詞公式表示出來，並且化為相應的子句集S。

② 把待求解的問題也用謂詞公式表示出來，然後把它的否定式與謂詞ANSWER構成一個析取式，ANSWER是一個為了求解問題而專設的謂詞，其變元數量和變元名必須與問題公式的變元完全一致。

③ 把此析取式化為子句集，並且把該子句集併入到子句集S中，得到子句集S′。

④ 對S′套用歸結原理進行歸結。

⑤ 若在歸結樹的根節點中僅得到歸結式ANSWER，則答案就在ANSWER中。

在歸結時並不要求把子句集中對歸結全部的子句都用到，只要在定理證明時能歸結出空子句，在求取問題答案時能歸結出ANSWER就可以了。另外，在歸結過程中，一個子句還可以多次被用來進行歸結。

歸結反演的改進策略

對子句集進行歸結反演時，由於事先不知道哪兩個子句可以進行歸結，更不知道通過對哪些子句對的歸結可以儘快地得到空子句，因而必須對子句集中的所有子句逐對地進行比較，對任何一個可歸結的子句對都進行歸結。也就是說，在子句集中採用了類似寬度優先搜尋方法來搜尋親本子句，因此歸結的效率很低。為此，研究了多種歸結反演的改進策略。這些歸結反演策略大致可分為兩大類：一類是刪除策略，另一類是限制策略。前一類通過刪除某些無用的子句來縮小歸結的範圍，後一類通過對參加歸結的子句進行種種限制，儘可能地減小歸結的盲目性，使其儘快地歸結出空子句。

刪除策略

歸結過程是一個不斷尋找可歸結子句的過程，子句越多，時空花費就越大。如果在歸結時先把子句集中對歸結無用的子句刪除掉，就會提高歸結的效率。刪除策略正是出於這一考慮提出來的，有以下幾種刪除策略。

1、純文字刪除

如果某文字L在子句集中不存在可與之互補的文字¬L，則稱該文字為純文字。顯然，在歸結時純文字不可能被消去，因而用包含它的子句進行歸結時不可能得到空子句，即這樣的子句對歸結是無意義的，所以可以把它所在的子句從子句集中刪去而不會影響子句集的不可滿足性。

2、重言式刪除

如果一個子句中同時包含互補文字時，則稱該子句為重言式。如：P(x)∨¬P(x)，P(x)∨Q(x)∨¬P(x)都是重言式。重言式是真值為真的子句。不管P(x)為真還是為假，P(x)∨¬P(x)以及P(x)∨Q(x)∨¬P(x)都均為真。對於一個子句集來說，增加或者刪去一個真值為真的子句都不會影響它的不可滿足性，因而可從子句集中刪去重言式。

3、包孕刪除

設有子句C₁和C₂，如果存在一個代換σ，使得C₁σ⊆C₂，則稱C₁包孕於C₂。把子句集中被包孕的子句刪去後，不會影響子句集的不可滿足性，因而可從子句集中刪去被其他子句包孕的子句。

限制策略

歸結的一般過程

設有初始子句集S={C₁，C₂，C₃，C₄}其中，C₁，C₂，C₃，C₄是S中的子句。對此子句集進行歸結的一般過程是：

① 從子句C₁開始，逐個與C₂，C₃，C₄進行比較，看哪兩個子句可進行歸結。若能找到，就求出歸結式。然後，用C₂與C₃、C₄進行比較，凡可歸結的都進行歸結。最後，用C₃與C₄比較，若能歸結也對它們進行歸結。經過這一輪的比較及歸結後，就會得到一組歸結式，稱為第一級歸結式。

② 再從C₁開始，用S中的所有子句分別與第一級歸結式中的子句逐個地進行比較、歸結，這樣又會得到一組歸結式，稱為第二級歸結式。

③ 仍然從C₁開始，用S中的所有子句及第一級歸結式中的所有子句逐個地與第二級歸結式中的子句進行比較，得到第三級歸結式。

如此繼續，只要子句集是不可滿足的，上述歸結過程直至歸結出空子句而終止。

1、支持集策略

支持集策略對參加歸結的子句提出了如下限制：每一次歸結時，親本子句中至少應有一個是由目標公式的否定所得到的子句，或者是它們的後裔。可以證明，支持集策略是完備的，即：若子句集是不可滿足的，則由支持集策略一定可以歸結出空子句。

2、線性輸入策略

線性輸入策略對參加歸結的子句提出了如下限制：參加歸結的兩個子句中必須至少有一個是初始子句集中的子句。初始子句集是由已知前提與結論的否定組成的子句集。線性輸入策略可限制生成歸結式的數量，具有簡單、高效的優點，但它是不完備的。也就是說，即使子句集是不可滿足的，用線性輸入策略進行歸結也不一定能歸結出空子句。

3、單文字子句策略

如果一個子句只包含一個文字，則稱它為單文字子句。單文字子句策略要求參加歸結的兩個子句中必須有一個是單文字子句。用單文字子句策略歸結時，歸結式將比親本子句含有較少的文字，這有利於朝著空子句的方向前進，因此它有較高的歸結效率。但是，這種歸結策略是不完備的。另外，當初始子句集中不包含單文字子句時，歸結就無法進行。

4、祖先過濾型策略

祖先過濾型策略與線性輸入策略比較相似，但放寬了限制。當對兩個子句C₁和C₂進行歸結時，要求它們滿足下述兩個條件中的任意一個條件：

①C₁與C₂中至少有一個是初始子句集中的子句。

② 如果兩個子句都不是初始子句集中的子句，則一個子句應是另一個子句的祖先。所謂一個子句（例如，C₁）是另一個子句（例如，C₂）的祖先是指C₂是由C₁與別的子句歸結後得到的歸結式。

以上幾種基本的歸結策略，在具體套用時可以組合在一起使用。