[發(fā)明專利]命題邏輯中基于最大矛盾體的自動推理方法

在審

• 申請?zhí)枺?/td>: 201710334627.4
• 申請日: 2017-05-12
• 公開（公告）號: CN108875939A
• 公開（公告）日: 2018-11-23
• 發(fā)明（設(shè)計）人: 徐揚;鐘小梅;劉軍;何星星;陳樹偉
• 申請（專利權(quán)）人: 西南交通大學(xué)
• 主分類號: G06N5/04
• 分類號: G06N5/04
• 代理公司: 成都天嘉專利事務(wù)所(普通合伙) 51211
• 代理人: 蔣斯琪

本發(fā)明公開了命題邏輯中基于最大矛盾體的自動推理方法，其步驟為：首先，利用子句集S中出現(xiàn)的k個變元生成最大矛盾體，然后利用最大矛盾體找出矛盾體，刪除矛盾體中的文字后，將全部剩余文字析取形成矛盾體分離式，最后利用矛盾體分離式判定子句集S的屬性，完成推理；本發(fā)明突破了傳統(tǒng)的歸結(jié)原理每次演繹“且只能有兩個子句參與”的限制，將靜態(tài)、二元、歸結(jié)演繹發(fā)展為動態(tài)、多元、矛盾體分離演繹，該方法具有更強的針對性、更大的靈活性，判定邏輯公式屬性的能力更強。

技術(shù)領(lǐng)域

本發(fā)明屬于基于邏輯的自動推理的技術(shù)領(lǐng)域，具體涉及命題邏輯中基于最大矛盾體的自動推理方法。

背景技術(shù)

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

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

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

基于語法的思想是解決其組合爆炸的可能途徑之一。1965年，J.A.Robinson從語法的角度提出了歸結(jié)原理。由于該推理規(guī)則的簡潔、可靠和完備性，基于歸結(jié)原理的自動推理系統(tǒng)很快成為自動推理領(lǐng)域中最著名最廣泛應(yīng)用的發(fā)展方向之一，至今已取得豐碩成果，并成為眾多著名自動推理系統(tǒng)的推理機制。其中最基本、最關(guān)鍵的推理機制是二元歸結(jié)——整個演繹過程中每次演繹“有，且只能有兩個子句參與”(盡管有集團歸結(jié)演繹、線性歸結(jié)演繹、鎖歸結(jié)演繹等方法，但其中的每一次演繹仍然如此)。二元歸結(jié)每次從待判定的子句集S中選取有互補對的兩個子句，從兩個子句中刪去該互補對，將剩余文字的析取構(gòu)成新的子句加入原子句集，重復(fù)如上過程，直至得到空子句，即可判定子句集S不可滿足。