歸結原理

歸結原理是由 Robinson (1965) 提出的，是一種定理證明方法，它透過構造反駁證明，即反證法來進行證明。這種方法已在許多自動定理證明器中得到應用。歸結原理適用於 一階邏輯 中 Skolem 正規化 的公式。這些公式基本上是 子句 的集合，其中每個子句是 文字 的 析取。合一 是歸結證明中的一項關鍵技術。

如果子句 中兩個或多個正文字（或兩個或多個負文字）是可合一的，且 是它們的最一般合一子，那麼 被稱為 的因子。例如， 被分解為 。在這種因子分解中，重複項被移除。

設 和 是兩個沒有公共變數的子句，設 包含一個正文字 ， 包含一個負文字 ，且設 是 和 的最一般合一子。那麼

被稱為 和 的二元歸結式。例如，如果 且 ，那麼 是它們的二元歸結式。

兩個子句 和 的歸結式是以下四種二元歸結式之一。

1. 和 的二元歸結式。

2. 和 的因子的二元歸結式。

3. 的因子和 的二元歸結式。

4. 的因子和 的因子的二元歸結式。

從兩個子句生成歸結式，稱為歸結，是歸結原理的唯一推理規則。歸結原理是完備的，因此，一個子句集合（合取）是 不可滿足的 當且僅當 可以透過歸結從它推匯出 空子句。

歸結原理完備性的證明基於 Herbrand 定理。由於不可滿足性與有效性是對偶的，因此歸結原理應用於定理的否定。

已經開發出多種策略來提高歸結原理的效率。這些策略有助於選擇子句對以應用歸結規則。例如，線性歸結是以下演繹策略。設 為子句的初始集合。如果 ，則從 線性演繹出 ，其中 頂子句 為 ，是指一種演繹，其中每個 是 和 () 的歸結式，並且每個 要麼在 中，要麼是一個歸結式 （其中 ）。

線性歸結是完備的，因此，如果 是不可滿足的子句集 中的一個子句，並且 是可滿足的，那麼可以透過以 作為 頂子句 的線性歸結獲得 空子句。

如果附加限制 必須在 中，那麼這種受限策略是不完備的。但是，對於包含 恰好一個 目標的 Horn 子句 集合，並且目標被選為 頂子句，它是完備的。此類集合中的所有其他子句都是確定的 Horn 子句。程式語言 Prolog 的實現就是在這種策略的框架內進行搜尋。