歸結原理

歸結（resolution）原理，在數理邏輯和自動定理證明中（GOFAI涉及的主題），是對於命題邏輯和一階邏輯中的句子的推理規則，它導致了一種反證法的定理證明技術。

命題邏輯中的歸結

歸結規則

在命題邏輯中的歸結規則是一個單一的有效的推理規則，從兩個子句生成它們所蘊含的一個新的子句。歸結規則接受包含互補的文字的兩個子句 - 子句是文字的析取式，並生成帶有除了互補的文字的所有文字的一個新子句。形式上，這裡的$a_{i}$和$b_{j}$是互補的文字：

${\frac {a_{1}\lor \ldots \vee a_{i-1}\vee a_{i}\vee a_{i+1}\vee \ldots \lor a_{n},\quad b_{1}\lor \ldots \vee b_{j-1}\vee b_{j}\vee b_{j+1}\vee \ldots \lor b_{m}}{a_{1}\lor \ldots \lor a_{i-1}\lor a_{i+1}\lor \ldots \lor a_{n}\lor b_{1}\lor \ldots \lor b_{j-1}\lor b_{j+1}\lor \ldots \lor b_{m}}}$

歸結規則生成的子句叫做兩個輸入子句的歸結（resolvent）。

當兩個子句包含多於一對的互補文字的時候，歸結規則可以（獨立的）應用到每個這種文字對上。但是，只有要消去（resolve）的文字對可以去除：所有其他文字對仍保留在歸結後的子句中。

一種歸結技術

當外加上完備的搜索算法的時候，歸結規則生成一個可靠的和完備的算法來決定命題公式的可滿足性，並且經過擴展，決定句子在一組公理下的有效性。

這種歸結技術使用反證法，並基於在命題邏輯中的任何句子都能轉換成等價的合取範式句子的事實。步驟如下：

• 在知識庫中所有句子和要證明的句子（猜測（conjecture）)的否定都合取連結。
• 結果的句子變換成合取範式（處理成一組子句）。
• 把歸結規則應用到包含互補的文字的所有可能的子句對，通過除去重複的文字來簡化結果的句子。如果句子包含互補的文字，則（作為重言式）丟棄它。如果沒有，並且它在子句的集合中仍然不存在，則增加上它，並考慮做進一步的歸結推理。
• 如果在應用歸結規則之後推導出空子句，則全部的公式是不可滿足的（或者說矛盾的），所以可以做出最初的猜測從這些公理中推出的結論。
• 在另一方面，如果不能推導出空子句，並且不能應用歸結規則推導更多的新子句，則這個猜測不是最初的知識庫的定理。

這個算法的一個實例是最初的Davis-Putnam算法，它後來被精製成去除了對歸結出的子句的顯式表示的需求的DPLL算法。

一階邏輯中的歸結

一階邏輯歸結把傳統的邏輯推理的直言三段論濃縮成了一個單一的規則。

要理解歸結是如何工作的，考慮詞項邏輯三段論的下列例子：

所有希臘人都是歐洲人。

荷馬是希臘人。

所以，荷馬是歐洲人。

或者，更一般性的：

∀X, P（X）→ Q（X）。

P（a）。

所以, Q（a）。

要使用歸結技術重造推理，首先子句們必須轉換成合取範式。在這種形式下，所有的量化都成為隱含的：在變量（X, Y...）上的全稱量詞理所當然的被省略了，而存在量化的變量被替換成Skolem函數。

¬P（X）∨ Q（X）

P（a）

所以, Q（a）

所以，問題是歸結技術如何從前兩個子句推導出最後一個子句?規則是簡單的：

• 找到包含相同謂詞的兩個子句，這個謂詞在一個子句中是否定的而在另一個子句中是肯定的。
• 在兩個謂詞上進行合一。（如果合一失敗，則你做了錯誤的謂詞選擇，回到前面的步驟再次嘗試。）
• 如果在被合一的謂詞中受到約束的任何未綁定的變量也出現這兩個子句中的其他謂詞中，則同樣的把它們替換（replace）成它們的綁定值（項）。
• 丟棄被合一的謂詞，並合併兩個子句中的餘下的謂詞到一個新子句中，並用"∨"算子連接起來。

要應用這個規則到上述例子，我們找到謂詞P以否定形式出現在第一個子句中

¬P（X）

並以非否定形式出現在第二個子句中

P（a）

X是一個未綁定變量，而a是一個綁定變量（原子）。合一兩個子句生成代換（substitution）

X := a

丟棄合一了的謂詞，並把這個代換應用到餘下的謂詞中（在本例中就是Q（X）)，生成結論：

Q（a）

舉個其他例子，考慮三段論形式

所有克里特島人都是島上居民。

所有島上居民都是說謊者。

所以，所有克里特島人都是說謊者。

或者更一般性的,

∀X P (X) → Q（X）

∀X Q (X) → R（X）

所以, ∀X P (X) → R（X）

在合取範式中，前提變成了：

¬P（X）∨ Q（X）

¬Q（Y）∨ R（Y）

（注意在第二個子句中的變量被重命名來使在不同子句中的變量清晰的區分開來。）

現在，合一第一個子句中的Q（X）和第二個子句中¬Q（Y）意味着X和Y變成了同一個變量。把這個變量代換到餘下的子句中，合併它們給出結論：

¬P（X）∨ R（X）

歸結規則（帶有額外的因數分解）同樣的包容傳統邏輯的所有其他的演繹形式。

Paramodulation

Paramodulation是一種相關技術，用於推理條款集，其中謂詞變量是平等的。它可以生成所有 "相等 "的子句，但反身的相同性除外。參數化操作需要一個正的從子句，它必須包含一個平等字面。然後，它搜索一個 "進入 "子句，該子句與平等關係的一方相統一。然後，該子項被等號的另一邊所取代。Paramodulation的一般目的是將系統簡化為原子，在替換時減少術語的大小。

參考文獻

• Robinson, J. Alan. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM. 1965, 12 (1): 23–41. doi:10.1145/321250.321253. 
• Leitsch, Alexander. The Resolution Calculus. Springer. 1997. 
• Gallier, Jean H. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers. 1986 [2018-08-16]. （原始內容存檔於2018-08-08）. 
• Lee, Chin-Liang Chang, Richard Char-Tung. Symbolic logic and mechanical theorem proving [reprint]. San Diego: Academic Press. 1987. ISBN 0-12-170350-9. 

Approaches to non-clausal resolution, i.e. resolution of first-order formulas that need not be in clausal normal form, are presented in:

• D. Wilkins. QUEST — A Non-Clausal Theorem Proving System (學位論文). Univ. of Essex, England. 1973. 
• Neil V. Murray. A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic (技術報告). Syracuse Univ. Feb 1979 [2018-08-16]. 2-79. （原始內容存檔於2020-06-07）.  (Cited from Manna, Waldinger, 1980 as: "A Proof Procedure for Non-Clausal First-Order Logic", 1978)
• Zohar Manna, Richard Waldinger. A Deductive Approach to Program Synthesis. ACM Transactions on Programming Languages and Systems. Jan 1980, 2: 90–121 [2018-08-16]. doi:10.1145/357084.357090. （原始內容存檔於2017-09-27）.  A preprint appearead in Dec 1978 as SRI Technical Note 177 （頁面存檔備份，存於網際網路檔案館）
• N. V. Murray. Completely Non-Clausal Theorem Proving. Artificial Intelligence. 1982, 18: 67–85. doi:10.1016/0004-3702(82)90011-x. 
• Schmerl, U.R. Resolution on Formula-Trees. Acta Informatica. 1988, 25: 425–438. doi:10.1007/bf02737109.  Summary （頁面存檔備份，存於網際網路檔案館）

外部連結

• Resolution Principle （頁面存檔備份，存於網際網路檔案館）
• Resolution （頁面存檔備份，存於網際網路檔案館）