基於格值邏輯的語言真值α-群鎖語義歸結自動推理研究

《基於格值邏輯的語言真值α-群鎖語義歸結自動推理研究》是依託西南交通大學，由鐘小梅擔任項目負責人的數學天元基金項目。

基本介紹

• 中文名：基於格值邏輯的語言真值α-群鎖語義歸結自動推理研究
• 項目類別：數學天元基金項目
• 項目負責人：鐘小梅
• 依託單位：西南交通大學

項目摘要

針對帶有不可比較性信息的自動推理，依據基於格蘊涵代數的格值邏輯系統，借鑑經典二值邏輯中語義歸結和鎖歸結自動推理的學術思想，在基於格蘊涵代數的格值邏輯的語言真值α-歸結自動推理研究基礎上，進一步研究基於格值命題邏輯系統LP(X)與一階邏輯系統LF(X)的語言真值α-群鎖語義歸結自動推理，提出相應的基本理論、並建立具有可靠性和完備性的方法。

結題摘要

為了處理帶有不可比較性信息的自動推理，在基於格蘊涵代數的格值命題邏輯系統LP(X)中，建立了α-群鎖語義歸結自動推理方法及其可靠性與條件完備性，進一步將該方法拓展到了相應的格值一階邏輯系統LF(X)中，並基於LF(X)證明了該方法的可靠性定理、提升引理與條件完備性定理。同時，分別將語言真值格值命題邏輯LV(n×2)P(X)與一階邏輯LV(n×2)F(X)中的α-群歸結原理、α-群鎖語義歸結等價轉化到了一個更簡單的格值命題邏輯LVnP(X)中。此外，基於格值命題邏輯LnP(X)給出了一些α-群歸結組的判定原則。這為進一步將語言真值α-歸結自動推理用於實際問題提供了一定的理論基礎。