歸結原理

在命題邏輯歸結原理的推理圖式中，P、Q和R稱為原子公式（簡稱原子），即不使用邏輯連接詞的簡單命題形式。原子和原子的否定式統稱句元，例如P與塡P、Q與塡Q、R與塡R即是三對互補句元。子句就是將不同句元用析取詞∨（或）連接而成的析取式。應用歸結法則進行推理時，所有判斷都寫成子句的形式，這不論對命題邏輯還是對一階謂詞邏輯都不例外。

在命題邏輯中，原子被看成一個內部結構不予分析的邏輯基元，代表簡單的命題形式。單憑普通形式邏輯中充分條件的假言聯鎖推理的符號化，只能直接演變為命題邏輯的歸結原理。命題邏輯的歸結原理或歸結法則可歸納如下：對任意兩個子句H1和H2，如果H1和H2中各自包含一個互補的句元L1和L2（例如上述圖式中的Q和塡Q），則可以刪去L1和L2，並將原來的子句H1與H2歸結為刪去互補句元后兩子句餘下部分的析取式C。C也以子句形式出現，稱為原來兩子句（常稱為親子句）的一個歸結式例如圖式中塡P∨R即為塡P∨Q與塡Q∨R兩子句的一個歸結式。歸結原理或歸結法則即因此得名。

一階謂詞邏輯中，原子是由謂詞和項組成的，因而在句元和子句中就有個體變元出現。由於存在量詞能用斯科林變換消去，可以認為句元和子句中的個體變元只受全稱量詞約束（見邏輯表示）。兩個子句H1與H2的歸結式可分四種情形：①子句H1與H2的歸結式；②子句H1與子句H2的因子句H2′的二元歸結式；③子句H1的因子句H1′與子句H2的二元歸結式；④子句H1、H2各自的因子句H1′與H2′的二元歸結式。求子句的因子句和求兩子句歸結式時，都必須用合一演演算法求出最普遍合一替換mgu（most general unifier），或稱最廣通代。這是在一階謂詞邏輯中應用歸結法則的關鍵技術，最普遍合一替換是在一個表達式集合E={E1，…，Ek}中，用一組項（t1，…，tk）替換一組互異個體變元（x1，…，xk），使替換后的各表達式相等（稱為合一）的最簡替換。①求子句因子句時的最普遍合一替換：例如子句H1=P(x）∨P(f(y））∨塡Q(x)的因子句H1′=P(f(y））∨塡Q(f(y）），mgu={f(y)/x}。②求兩子句（包括子句之一或兩子句都有因子句的情形）的二元歸結式時的最普遍合一替換：例如子句H 2=塡P(f(g(a））∨R(b），則H2與上例H1的因子句H1′的二元歸結式C=塡Q(f(g(a））∨R(b),mgu={g(a)/y}。

應用歸結原理證明定理或求解問題時採用反證法，即先假設與結論相反的命題是成立的，然後根據前提和否定結論的假設（都以子句形式出現），求出一系列中間結論（以歸結式的形式出現），如果最後得到兩個相互矛盾的命題（以互補句元形式出現的一對單句元子句），即表明與結論相反的假設不能成立，因而原結論的正確性得證，此時歸結式是空子句□。可以從理論上證明一階謂詞邏輯的歸結原理是完備的，即一個子句集S（前提和結論否定式合取形成的全體子句）不可滿足的充要條件是從子句集S中能推導出空子句。

應用歸結法則的具體步驟是：①將定理或問題用邏輯形式表示。②消去存在量詞，使公式中出現的所有個體變元只受全稱量詞約束。③構造子句集，包括將所有前提表示為子句形式；將結論否定也表示為子句形式。④證明子句集S的不可滿足性，即應用歸結法則和合一演演算法，反覆推求兩子句的歸結式（對命題邏輯情形無需採用合一演演算法），直到最終推導出空子句□，即表明定理得證或問題有解。這個推理過程由計算機自動進行。

表說明歸結法則在自動演繹中的應用。

根據歸結原理進行推理時只需要一條推理規則，即求兩子句歸結式的歸結法則，所以使用簡便，容易在計算機上實現。後來發現對於複雜的推理問題，中間歸結式的產生會陷入盲目狀態，缺乏可以明確遵循的搜索策略，使推理效率大為降低。為此又提出一些改進方案，如語義歸結、鎖歸結、線性歸結等，此外還對廣義歸結進行了研究。