命題邏輯
歸結原理在命題邏輯中，原子被看成一個內部結構不予分析的邏輯基元，代表簡單的命題形式。單憑普通形式邏輯中充分條件的假言聯鎖推理的符號化，只能直接演變為命題邏輯的歸結原理。命題邏輯的歸結原理或歸結法則可歸納如下：對任意兩個子句H1和H2，如果H1和H2中各自包含一個互補的句元L1和L2（例如上述圖式中的Q和塡Q），則可以刪去L1和L2，並將原來的子句H1與H2歸結為刪去互補句元後兩子句餘下部分的析取式C。C也以子句形式出現，稱為原來兩子句（常稱為親子句）的一個歸結式例如圖式中塡P∨R即為塡P∨Q與塡Q∨R兩子句的一個歸結式。歸結原理或歸結法則即因此得名。
基本思想
從套用的角度出發，可以從充分條件的假言聯鎖推理、命題邏輯的歸結原理，一階謂詞邏輯的歸結原理等三個方面來分析歸結原理的基本思想。充分條件的假言聯鎖推理 是前提和結論全部由充分條件假言判斷構成的一種推理形式。下面是普通形式邏輯中在引入蘊涵連線詞“→”（代表如果……則……的邏輯關係）後的推理圖式：
由於P→Q (如果P 則Q)和
（非P或Q）這兩個公式邏輯等價，即（P→Q）呏（塡P∨Q）,同理有（Q→R）呏（塡Q∨R）,（P→R）呏（塡P∨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的歸結式;②子句H 1與子句H2的因子句H2′的二元歸結式；③子句H 1的因子句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的不可滿足性,即套用歸結法則和合一算法，反覆推求兩子句的歸結式（對命題邏輯情形無需採用合一算法）,直到最終推導出空子句□,即表明定理得證或問題有解。這個推理過程由計算機自動進行。
套用舉例
表說明歸結法則在自動演繹中的套用。根據歸結原理進行推理時只需要一條推理規則，即求兩子句歸結式的歸結法則，所以使用簡便，容易在計算機上實現。後來發現對於複雜的推理問題，中間歸結式的產生會陷入盲目狀態，缺乏可以明確遵循的搜尋策略,使推理效率大為降低。為此又提出一些改進方案,如語義歸結、鎖歸結、線性歸結等，此外還對廣義歸結進行了研究。
