標籤: 暫無標籤

歸結原理是將普通形式邏輯中充分條件的假言聯鎖推理形式符號化,並向一階謂詞邏輯推廣的一種推理法則,又稱歸結法則、分解法則、消解法則。

1 歸結原理 -歸結原理

 

2 歸結原理 -正文

  將普通形式邏輯中充分條件的假言聯鎖推理形式符號化,並向一階謂詞邏輯推廣的一種推理法則,又稱歸結法則、分解法則、消解法則。
  基本思想  從應用的角度出發,可以從充分條件的假言聯鎖推理、命題邏輯的歸結原理,一階謂詞邏輯的歸結原理等三個方面來分析歸結原理的基本思想。
  充分條件的假言聯鎖推理  是前提和結論全部由充分條件假言判斷構成的一種推理形式。下面是普通形式邏輯中在引入蘊涵連接詞「→」(代表如果……則……的邏輯關係)后的推理圖式:

歸結原理

橫線上、下方的邏輯公式分別與推理的前提和結論相對應。
  由於PQ(如果PQ)和歸結原理(非PQ)這兩個公式邏輯等價,即(PQ)呏(塡P∨Q),同理有(QR)呏(塡Q∨R),(PR)呏(塡P∨R)。用這些邏輯等價關係的右式分別替換其中的蘊涵公式,即得命題邏輯中使用歸結法則的推理圖式:

歸結原理

  命題邏輯的歸結原理  在命題邏輯歸結原理的推理圖式中,PQR稱為原子公式(簡稱原子),即不使用邏輯連接詞的簡單命題形式。原子和原子的否定式統稱句元,例如P與塡PQ與塡QR與塡R即是三對互補句元。子句就是將不同句元用析取詞∨(或)連接而成的析取式。應用歸結法則進行推理時,所有判斷都寫成子句的形式,這不論對命題邏輯還是對一階謂詞邏輯都不例外。
  在命題邏輯中,原子被看成一個內部結構不予分析的邏輯基元,代表簡單的命題形式。單憑普通形式邏輯中充分條件的假言聯鎖推理的符號化,只能直接演變為命題邏輯的歸結原理。命題邏輯的歸結原理或歸結法則可歸納如下:對任意兩個子句H1和H2,如果H1和H2中各自包含一個互補的句元L1和L2(例如上述圖式中的Q和塡Q),則可以刪去L1和L2,並將原來的子句H1與H2歸結為刪去互補句元后兩子句餘下部分的析取式CC也以子句形式出現,稱為原來兩子句(常稱為親子句)的一個歸結式例如圖式中塡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}。②求兩子句(包括子句之一或兩子句都有因子句的情形)的二元歸結式時的最普遍合一替換:例如子句H2=塡P(f(g(a))∨R(b),則H2與上例H1的因子句H1′的二元歸結式C=塡Q(f(g(a))∨R(b),mgu={g(a)/y}。
  應用方法  應用歸結原理證明定理或求解問題時採用反證法,即先假設與結論相反的命題是成立的,然後根據前提和否定結論的假設(都以子句形式出現),求出一系列中間結論(以歸結式的形式出現),如果最後得到兩個相互矛盾的命題(以互補句元形式出現的一對單句元子句),即表明與結論相反的假設不能成立,因而原結論的正確性得證,此時歸結式是空子句□。可以從理論上證明一階謂詞邏輯的歸結原理是完備的,即一個子句集S(前提和結論否定式合取形成的全體子句)不可滿足的充要條件是從子句集S中能推導出空子句□。
  實施步驟  應用歸結法則的具體步驟是:①將定理或問題用邏輯形式表示。②消去存在量詞,使公式中出現的所有個體變元只受全稱量詞約束。③構造子句集,包括將所有前提表示為子句形式;將結論否定也表示為子句形式。④證明子句集S的不可滿足性,即應用歸結法則和合一演算法,反覆推求兩子句的歸結式(對命題邏輯情形無需採用合一演算法),直到最終推導出空子句□,即表明定理得證或問題有解。這個推理過程由計算機自動進行。
  應用舉例  表說明歸結法則在自動演繹中的應用。

歸結原理歸結原理

  根據歸結原理進行推理時只需要一條推理規則,即求兩子句歸結式的歸結法則,所以使用簡便,容易在計算機上實現。後來發現對於複雜的推理問題,中間歸結式的產生會陷入盲目狀態,缺乏可以明確遵循的搜索策略,使推理效率大為降低。為此又提出一些改進方案,如語義歸結、鎖歸結、線性歸結等,此外還對廣義歸結進行了研究。
  參考書目
 中國人民大學哲學系邏輯教研室編:《形式邏輯》,中國人民大學出版社,北京,1984。Ching-Liang Chang and Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving,Academic Press,Inc.,New York,1973.

 

3 歸結原理 -配圖

 

4 歸結原理 -相關連接

相關評論

同義詞:暫無同義詞