基于格值邏輯的α-多元線性歸結自動推理研究.pdf

1、人工智能領域中的一個極具有挑戰(zhàn)性的研究方面是自動推理（定理機器證明），歸結自動推理是自動推理的重要研究方向之一，其研究成果已被應用到很多重要領域，如人工智能、邏輯編程、問題求解、軟件模型檢測與測試、安全協(xié)議、程序自動驗證、應答系統(tǒng)等方面。現(xiàn)實世界中經(jīng)常遇到一些由于其多因素而產(chǎn)生不可比較性的問題，這類帶有不可比較性信息的問題往往很復雜?；诟裉N涵代數(shù)的格值邏輯系統(tǒng)的歸結自動推理是解決這類問題的有效方法之一。
　　本文在其他學者的工作

2、基礎上，依據(jù)經(jīng)典邏輯的歸結推理方法，對基于格蘊涵代數(shù)的格值邏輯系統(tǒng)的α-多元線性歸結自動推理的理論、方法、算法、程序展開研究。取得的研究成果主要有以下五個方面:
　　第一部分，在基于(L)ukasiewicz蘊涵代數(shù)Ln的格值命題邏輯系統(tǒng)LnP(X)中，得到了一類3階不可分極簡式(3-IESF)所有可能的形式，針對其中一類特別重要的3-IESF，給出了它與n-IESF(0≤n≤3)之間的α-可歸結性。
　　第二部分，在基于格

3、值邏輯系統(tǒng)的α-多元歸結原理的基礎上，針對廣義文字所有分類的分界廣義文字，給出了它們之間任意三個廣義文字的α-可歸結性，進一步得到了格值邏輯系統(tǒng)中的α-多元歸結域的一些性質。
　　第三部分，進一步在基于格值命題邏輯系統(tǒng)LP(X)的α-多元歸結原理基礎之上，提出了基于格值命題邏輯系統(tǒng)LP(X)的α-多元極小歸結原理，建立了LP(X)中的α-多元極小歸結原理的可靠性和完備性。然后，基于LP(X)的α-多元極小歸結原理，建立了基于LP(

4、X)的α-多元有序線性極小歸結方法，并建立了基于LP(X)的α-多元有序線性極小歸結方法的可靠性和條件完備性定理，分析了基于LP(X)的α-多元有序線性極小歸結方法的有效性。進一步，構造了基于LP(X)的α-多元有序線性極小歸結自動推理算法，為了提升該算法的歸結效率，給出了廣義子句集預處理的方法和選取廣義文字及判定時的六個策略，然后證明了α-多元有序線性極小歸結自動推理算法的可靠性和完備性，對該自動推理算法的時間復雜度進行了分析，給出了

5、一個例子進行闡述算法的有效性，設計了基于LP(X)的α-多元有序線性極小歸結自動推理程序。
　　第四部分，提出了基于格值一階邏輯系統(tǒng)LF(X)的α-多元極小歸結原理，得到相應的提升引理，并證明了基于LF(X)的α-多元極小歸結原理是可靠和完備的，進而得到了α-多元極小歸結原理的等價轉換定理。然后，基于LF(X)的α-多元極小歸結原理，建立了基于LF(X)的α-多元有序線性極小歸結方法，并建立了基于LF(X)的α-多元有序線性極小歸

6、結方法的可靠性和條件完備性定理，得到了α-多元有序線性極小歸結方法的等價轉換定理，分析了基于LF(X)的α-多元有序線性極小歸結方法的有效性。進一步，構造了基于LF(X)的α-多元有序線性極小歸結自動推理算法，證明了該算法是可靠且完備的，并給出了一個例子進行闡述α-多元有序線性極小歸結算法的有效性。
　　第五部分，為了進一步提高α-歸結能力和歸結效率，針對廣義文字歸結的α-多元極小歸結進一步提升，提出了基于格值命題邏輯系統(tǒng)LP(X

7、)的非子句α-多元極小廣義歸結原理，并證明了該廣義歸結原理是可靠和完備的。提出了基于LP(X)的非子句α-多元有序線性廣義歸結方法，得到其可靠性和條件完備性。然后，基于非子句α-多元有序線性廣義歸結方法，構造了LP(X)中的一個非子句α-多元有序線性廣義歸結算法。進一步，將基于格值命題邏輯系統(tǒng)LP(X)的非子句α-多元極小廣義歸結原理推廣到LF(X)中，提出了基于格值一階邏輯系統(tǒng)LF(X)的非子句α-多元極小廣義歸結原理，給出了相應的提