[發明專利]命題邏輯中基于矛盾體分離的多元動態自動演繹推理方法

在審

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

本發明公開了命題邏輯中基于矛盾體分離的多元動態自動演繹推理方法，對于命題邏輯中子句集S，在S中選出k個子句C_j1，C_j2，…，C_jk，滿足C_j1，C_j2，…，C_jk含有矛盾體；第二步，在子句C_j1，C_j2，…，C_jk中刪除矛盾體中的文字，將全部剩余文字進行析取形成矛盾體分離式；最后，判定子句集S的屬性：若得出判定結果，則停止，否則，將矛盾體分離式并入S中得到新子句集，并對新子句集執行前兩步，直到得出結果。該方法可同時使用子句集中的多個甚至全部子句參與演繹，在更大程度上刻畫了多子句之間的整體協同邏輯關系，是將靜態的、二元的歸結演繹推理機制改進推廣成為動態的、多元的基于矛盾體分離的演繹推理機制。

技術領域

本發明涉及基于邏輯的自動演繹推理的技術領域，具體涉及命題邏輯中基于矛盾體分離的多元動態自動演繹推理方法。

背景技術

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

根據上述背景知識，自動推理是用于判定形式化為邏輯公式的實際問題的屬性。命題邏輯中最基本的公式為原子，原子x或原子的非(即“原子的否定”)～x稱為文字，如果兩個文字中一個是另外一個的非，則稱它們互補，或稱其為互補對。有限個文字的析取(即文字之間的關系為“或者”的關系)稱為子句，記子句C＝x₁∨x₂∨···∨x_k，其中x_i(i＝1，2，…，k)是一個文字。只含有一個文字的子句稱為單元子句，不含文字的子句稱為空子句，記為φ。一個邏輯公式S可以化為合取范式，即有限個子句的合取(即子句之間的關系為“并且”的關系)，記為S＝C₁∧···∧C_m，同時也可將S看作是一個子句集S＝{C₁，C₂，…，C_m}，其中C₁，C₂，…，C_m是子句。公式的真假性(一般用0表示假，1表示真)通過語義解釋實現。(語義)解釋通過對公式中所有原子賦以0或者1，再通過原子間的邏輯運算(非、析取、合取等)即可得到整個公式的真假性。如果一個公式在某解釋下的真值為1，則稱其為可滿足的，如果在任意解釋下的真值都為0，則稱其為不可滿足的，約定空子句為不可滿足的。

目前，主流的判定命題邏輯公式屬性的方法是基于語義的思想，如二叉樹、基于沖突的子句學習方法(CDCL)等。運用語義思想判定邏輯公式屬性會執行許多不必要的求解，也必然會產生組合爆炸。因此，為了解決該問題，許多研究者提出了各種各樣的策略，如子句學習、非時序回溯、啟發式分支決策、重啟、子句刪除等策略，同時，也有一些研究者研究求解各種特殊問題以適用于各種具體應用，但其普適性相對較弱。