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

在審

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

本發明公開了一階邏輯中基于矛盾體分離的多元動態自動演繹推理方法，該方法通過在一階邏輯中的子句集S中尋找標準矛盾體，然后在子句集S中剩余的子句中刪除出現在標準矛盾體中的文字，并將全部剩余文字進行析取形成矛盾體分離式，最后根據矛盾體分離式判定初始的子句集S的屬性，最終直到得出判定結果，則停止演繹推理。本發明可將靜態的、二元的歸結演繹推理機制改進推廣成為動態的、多元的基于矛盾體分離的演繹推理機制，可應用于系統可信性自動驗證、定理機器證明等領域，具有多元性、動態性、并行性、協調性、導向性、靈活性、方便性等特點。

技術領域

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

背景技術

邏輯學、數學、系統優化、人工智能、計算機科學等領域大量的科學問題都可形式化為邏輯表示，解決這些問題的本質之一就是對相應邏輯公式屬性(可滿足性或不可滿足性(恒假性))的判定，但因其抽象性、復雜性、規模性，無法人工有效地實現邏輯推理與求解，因而需要借助于計算機自動對其判定。自動推理是將推理過程通過一系列符號而形式化，使計算機自動地按某種規則對這些符號實施一系列演算的過程，它是一種智能化行為。先進的基于邏輯的自動推理理論、方法與系統可為解決這些高度復雜的問題提供嚴謹、快速的邏輯證明科學手段，可使機器類似于人類證明定理一樣自動地、系統地、嚴格地按照邏輯規則推理證明邏輯公式的屬性。這種方法和系統是基本的、必需的、科學的、系統的、普適的工具，也是極其難于構造的工具，可廣泛應用于所有基于邏輯的各應用領域的邏輯問題判定。

如前所述，自動推理用于判定形式化為邏輯公式的實際問題的屬性。一階邏輯中最基本的公式為原子，原子P(t₁，t₂，…，t_n)或原子的非(即“原子的否定”)～P(t₁，t₂，…，t_n)稱為文字，如果兩個文字中一個是另外一個的非，則稱它們互補，或稱其為互補對。有限個文字的析取(即文字之間的關系為“或者”的關系)稱為子句，只含有一個文字的子句稱為單元子句，不含文字的子句稱為空子句，記為φ。一階邏輯中的一個子句集S理解為如下一階邏輯中的公式：S中的所有子句合取起來，并將S中的每個變元都看作具有全稱量詞約束的。公式的真假性(一般用0表示假，1表示真)通過語義解釋實現。(語義)解釋通過對公式中所有的常元符號、函數符號、謂詞符號的指派，以及原子間的邏輯運算(非、析取、合取等)即可得到整個公式的真假性。如果一個公式在某解釋下的真值為1，則稱其為可滿足的，如果在任意解釋下的真值都為0，則稱其為不可滿足的，約定空子句為不可滿足的。

自1959年，王浩從邏輯演繹的過程中總結出推導規則，用計算機證明了《數學原理》中的220個定理，并于1960年在《IBM研究與發展年報》發表了“邁向數學機械化”(TowardMechanical Mathematics)一文以來，基于邏輯的自動演繹推理系統得到了快速發展，特別是1965年J.A.Robinson提出了歸結原理(Resolution Principle)之后，基于歸結原理的自動演繹推理系統很快成為自動演繹推理領域中最著名最廣泛應用的發展方向之一，至今已取得豐碩成果，并成為許多著名自動演繹推理系統的推理機制。

盡管如此，但基于歸結原理的自動演繹推理系統在能力與效率方面仍遠不能滿足客觀需要，僅國際著名問題庫TPTP中就有大量最難(Rating 1)的問題至今沒有解決，其中最基本、最關鍵的推理機制是二元歸結——整個演繹過程中每次演繹“有，且只能有兩個子句參與”(盡管有集團歸結演繹、線性歸結演繹、鎖歸結演繹等方法，但其中的每一次演繹仍然如此)，這一推理機制嚴重地制約著自動演繹推理的能力與效率進一步提高。因此，若能突破每次演繹“有，且只能有兩個子句參與”這一苛刻的限制，將靜態、二元、歸結演繹發展為動態、多元、矛盾體分離演繹，系統地建立可多子句同時參與的動態自動演繹——基于矛盾體(即多個子句共同形成的不可滿足子句集)分離的動態自動演繹推理的理論及其相應的方法與系統，必將從本質上可極大提升基于邏輯的自動演繹推理的能力與效率。

發明內容