基於格值邏輯的α-n(t)元歸結動態自動推理研究

《基於格值邏輯的α-n(t)元歸結動態自動推理研究》是依託西南交通大學，由徐揚擔任項目負責人的面上項目。

基本介紹

• 中文名：基於格值邏輯的α-n(t)元歸結動態自動推理研究
• 項目類別：面上項目
• 項目負責人：徐揚
• 依託單位：西南交通大學

項目摘要

針對帶有不可比較性信息的自動推理，依據基於格蘊涵代數的格值邏輯系統，借鑑基於經典二值邏輯的0-2元歸結自動推理的學術思想，在基於格蘊涵代數的格值邏輯的α-2元歸結自動推理研究基礎上，分別建立基於格值命題邏輯LP(X)和格值一階邏輯LF(X)、格值分層、群組歸結、動態演繹、效率提高、從本質上發展歸結自動推理的α-n(t)元歸結動態自動推理具有可靠性與完備性的理論、方法、算法和程式。

結題摘要

針對帶有不可比較性信息的自動推理，在基於格蘊涵代數的格值邏輯系統中，於α-n(t)元歸結動態自動推理理論、方法、算法和程式方面取得如下主要結果，這將為處理帶有不可比較性信息的自動推理研究與套用提供基礎及手段。 在格值命題邏輯LP(X)中：建立了子句型和非子句型的α-n(t)元歸結動態自動推理理論，給出了α-n(t)元歸結演繹中廣義文字個數動態變化的基本原則、α-n(t)元可歸結式集合的結構；建立了α-極小歸結、α-有序線性歸結和α-廣義語義歸結；在語言真值格值邏輯中建立了α-廣義鎖歸結理論。提出了α-n(t)元語義歸結方法，構造了算法，設計了程式；建立了非子句α-n(t)元有序線性廣義歸結方法；建立了α-有序線性極小歸結方法、α-半鎖語義歸結方法、α-n(t)元鎖歸結方法、α-n(t)元準鎖語義歸結方法、α-n(t)元語義歸結方法，在(Ln×L2)P(X)中構造了α-n(t)元準鎖語義歸結算法；基於LV(n×2)P(X)提出了α-線性歸結方法並構造了算法；設計了α-有序線性歸結算法；基於語言真值格值邏輯，提出了α-廣義鎖歸結自動推理方法；建立了α-廣義線性半鎖歸結方法，構造了算法。在L2P(X)中形成了0-n(t)元歸結動態自動推理方法、算法、程式雛形，基於此形成了C程式驗證工具Scavel C初級版，並已用於航空航天、武器裝備、軌道交通等領域，驗證程式150多萬行，為完善C程式初現其獨有作用。 在格值一階邏輯LF(X)中：建立了子句型和非子句型α-n(t)元歸結動態自動推理理論；給出了α-n(t)元歸結演繹中廣義文字個數動態變化的基本原則；建立了α-極小歸結原理、基於理想的歸結原理和α-廣義歸結原理；在 (Ln×L2)F(X)中，將α-歸結原理的一般形式等價轉化到了LnP(X)中。建立了α-n(t)元語義歸結動態自動推理方法，構造了算法，並指出：可將LP(X)的α-n(t)元語義歸結自動推理程式套用於LF(X)的α-n(t)元語義歸結自動推理；提出了α-有序線性歸結，構造了算法；建立了非子句α-n(t)元有序線性廣義歸結方法；建立了α-n(t)元準鎖語義歸結方法；建立了α-廣義線性半鎖歸結方法，構造了算法；針對L9x2F(X)設計了α-語義歸結自動推理程式；在L2F(X)中形成了0-n(t)元歸結動態自動推理方法、算法、程式雛形，基於此已證明4800多個定理。