Robinson第一定理

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

基本介紹

• 中文名：Robinson第一定理
• 外文名：J.A. Robinson's resolution Principle
• 別名：歸結原理
• 提出者：J.A. Robinson

命題邏輯中的歸結

歸結規則

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

歸結規則生成的子句叫做兩個輸入子句的歸結（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）。

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