《基於格值邏輯的α-鎖歸結與α-鎖調解自動推理》是依託西南交通大學，由何星星擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於格值邏輯的α-鎖歸結與α-鎖調解自動推理
- 項目類別：青年科學基金項目
- 項目負責人：何星星
- 依託單位：西南交通大學
項目摘要,結題摘要,
項目摘要
本項目圍繞帶等詞的格值邏輯系統，研究啟發式動態配鎖策略下的α-鎖歸結與α-鎖調解自動推理理論、方法和算法，設計相應的自動推理程式。主要內容包括：一、研究格值命題邏輯系統中廣義文字的結構、典型類廣義文字的歸結域及其歸結文字個數的選擇。二、針對α-鎖歸結與α-廣義鎖歸結方法，提出啟發式動態配鎖策略。在該策略下，分別建立兩種鎖歸結方法的可靠性與完備性。三、針對帶等詞的邏輯公式，建立基於格值一階邏輯的α-鎖調解自動推理理論和方法，並建立該調解方法在啟發式動態配鎖策略下的可靠性與完備性。四、針對上述理論和方法，設計基於格值邏輯的自動推理程式。項目預期的成果有望為基於格值邏輯的自動推理研究提供新的思路，為定理機器證明、形式化驗證等套用方面提供理論基礎和實用工具。
結題摘要
為處理含不確定性特別是不可比較性的信息提供了有效工具，本項目基於格值邏輯系統與自動推理理論，針對帶等詞的格值邏輯公式，建立了高效的α-（廣義）鎖歸結和α-鎖調解自動推理理論和方法，設計了相應的自動推理程式。研究成果主要包括以下三個方面： 基於格值邏輯的廣義文字的結構及其α-可歸結性的研究。具體為：給出了L_6P(X)上邏輯公式的性質，並得到了該邏輯系統中判斷公式是否為k階IESF的規則。進一步地，得到了尋找所有k階IESF的統一算法。給出了基於格值命題邏輯LP(X)的多元α-歸結式集合的代數結構，以及3個廣義文字的α-可歸結性的判定方法。給出了LP(X)中多元α-歸結演繹中參與多元-歸結的廣義文字個數隨歸結演繹動態變化的基本原則。 基於格值邏輯的α-（廣義）鎖歸結、α-鎖調解理論與方法的研究。具體為：建立了基於格值邏輯的多元α-語義歸結、α-準鎖語義歸結、α-半鎖語義歸結、α-群鎖歸結、非子句多元α-有序線性廣義歸結、α-有序（線性）極小歸結和α-有序語義歸結自動推理理論與方法，包括其可靠性、完備性及其相容性。給出了基於格值邏輯的合適歸結水平集，證明了在合適歸結水平下等詞公理與E解釋的等價性，以及邏輯公式不可滿足性的等價轉換。提出了α-調解原理與的概念，建立了α-調解原理的可靠性與完備性。給出了基於格值邏輯的α-GH調解的定義，證明了α-GH調解的可靠性與完備性。基於格值邏輯的實用證明器的實現。具體為：選擇典型的格值命題邏輯系統，設計了相應的證明器。驗證了一批格值邏輯公式，初步顯現了α-鎖歸結和α-鎖調解自動推理方法的優勢。進一步地，將研究成果推廣至經典二值邏輯中，並形成了多個基於二值邏輯的自動定理證明器。利用這些證明器證明了TPTP問題庫、Mizar問題庫中25萬餘個定理，特別是證明了rating 1的定理（其它證明器均未能成功證明）69個，初步顯現證明器的能力。這為定理機器證明、形式化驗證等套用方面提供理論基礎和套用工具。
