[發明專利]命題邏輯中基于標準延拓三角形的矛盾體分離演繹推理

在審

• 申請號: 201710335313.6
• 申請日: 2017-05-12
• 公開（公告）號: CN108875942A
• 公開（公告）日: 2018-11-23
• 發明（設計）人: 徐揚;何星星;陳樹偉;鐘小梅;劉軍
• 申請（專利權）人: 西南交通大學
• 主分類號: G06N5/04
• 分類號: G06N5/04
• 代理公司: 成都天嘉專利事務所(普通合伙) 51211
• 代理人: 蔣斯琪

本發明提出了命題邏輯中基于標準延拓三角形的矛盾體分離演繹推理，該方法依次通過：構造基于標準延拓三角形矛盾體；形成矛盾體分離式；根據矛盾體分離式和子句的特點判定子句集屬性，如果能夠判斷子句集不可滿足或可滿足，則停止；否則，將所得矛盾體分離式加入原子句集，形成新的子句集。接著構造并分離基于標準延拓三角形矛盾體，直至滿足條件停止或得到子句集屬性的判定結論。本發明可高效構造矛盾體，實現將靜態的、二元的歸結演繹推理機制改進推廣成為動態的、多元的基于矛盾體分離的演繹推理機制，是自動演繹推理領域一個本質性的突破。

技術領域

本發明涉及系統可信性自動驗證的技術領域，特別是命題邏輯中基于標準延拓三角形的矛盾體分離演繹推理。

背景技術

邏輯學、數學、系統優化、人工智能、計算機科學等領域大量的科學問題都可形式化為邏輯表示，這些問題正確性保證的本質是對相應邏輯公式屬性(可滿足性或不可滿足性(恒假性))的判定，但因其抽象性、復雜性、規模性，無法人工有效地實現邏輯推理與求解，因而需要借助于計算機對其判定。自動推理是將推理過程通過一系列符號而形式化，使計算機自動地按某種規則對這些符號實施一系列演算的過程，是一種智能化行為。先進的基于邏輯的自動推理理論、方法與系統可為解決這些高度復雜的問題提供嚴謹、快速的邏輯證明科學手段。它可使機器類似于人類證明定理一樣自動地、系統地、嚴格地按照邏輯規則推理證明邏輯公式的屬性，是一個基本的、必需的、科學的、系統的、普適的工具，也是極其難于構造的工具。它可廣泛應用于所有基于邏輯的各應用領域的邏輯問題判定，如，軟件生成與驗證，邏輯電路驗證，通信協議驗證，知識庫相容性驗證，大型數據庫維護，交通運輸，社會管理決策，信息系統安全等。

如前所述，自動推理用于判定形式化為邏輯公式的實際問題的屬性。命題邏輯中最基本的公式為原子，原子x或原子的非(即“否定”)～x稱為文字，如果兩個文字中一個是另外一個的非，則稱它們為互補對。有限個文字的析取稱為子句，記為C＝x₁∨x₂∨…∨x_k，其中x_i是一個文字。只含有一個文字的子句稱為單文字子句。不含文字的子句稱為空子句。一個邏輯公式可以化為合取范式，即有限個子句的合取，記為S＝C₁∧…∧C_m。轉化為合取范式的公式也稱為子句集，記為S＝{C₁,C₂,…,C_m}。公式的真假性(一般用0表示假，1表示真)通過語義解釋實現。(語義)解釋通過對公式中所有原子賦以0或者1，再由原子間的邏輯運算(非、析取、合取等)即可得到整個公式的真假性。設空子句的真值恒為“假(0)”。如果一個公式在某一解釋下真值為1，則稱它為可滿足的，同時稱該解釋為一個可滿足解釋。如果一個公式在任意解釋下的真值都為0，則稱其為不可滿足的或不可滿足的。公式可滿足的情況下，可從它的每個子句中至少找到一個均賦值為1的文字，這組文字稱為該公式或子句集的可滿足例。

對命題邏輯公式的屬性判定主要有完備性方法和不完備性方法兩類。完備性方法的優點是保證能正確地判定公式屬性，但其計算效率很低，平均的計算時間為多項式階，最差情況的計算時間為指數階，不適用于判定大規模的邏輯公式；不完備性方法的優點是求解比完備性方法快得多，但在許多情況下不能正確、甚至無法判定公式的屬性。目前，針對命題邏輯公式的屬性判定的許多方法是基于語義的思想，如二叉樹、基于沖突的子句學習方法(CDCL)等。但用語義思想對其判定時，會執行許多不必要求解，也必然會產生組合爆炸。因此，許多研究者提出了各種各樣的策略，如，子句學習、非時序回溯、啟發式分支決策、重啟策略、子句刪除等策略，以減少不必要的求解。這其中很多方法屬于不完備性方法。也有許多研究者研究各種求解特殊問題以適用于各種具體應用，但其普適性相對較弱。