[科普中國]-歸結(jié)原理

歸結(jié)（resolution）原理，在數(shù)理邏輯和自動定理證明中（GOFAI涉及的主題），是對于命題邏輯和一階邏輯中的句子的推理規(guī)則，它導(dǎo)致了一種反證法的定理證明技術(shù)。將普通形式邏輯中充分條件的假言聯(lián)鎖推理形式符號化，并向一階謂詞邏輯推廣的一種推理法則，又稱歸結(jié)法則、分解法則、消解法則。

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

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

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

應(yīng)用方法應(yīng)用歸結(jié)原理證明定理或求解問題時采用反證法，即先假設(shè)與結(jié)論相反的命題是成立的，然后根據(jù)前提和否定結(jié)論的假設(shè)（都以子句形式出現(xiàn)），求出一系列中間結(jié)論（以歸結(jié)式的形式出現(xiàn)），如果最后得到兩個相互矛盾的命題（以互補句元形式出現(xiàn)的一對單句元子句），即表明與結(jié)論相反的假設(shè)不能成立，因而原結(jié)論的正確性得證，此時歸結(jié)式是空子句□?？梢詮睦碚撋献C明一階謂詞邏輯的歸結(jié)原理是完備的，即一個子句集 S（前提和結(jié)論否定式合取形成的全體子句）不可滿足的充要條件是從子句集S 中能推導(dǎo)出空子句。1

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

應(yīng)用舉例表說明歸結(jié)法則在自動演繹中的應(yīng)用。

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

本詞條內(nèi)容貢獻者為:

程鵬 - 副教授 - 西南大學(xué)