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

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

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

背景技術(shù)

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

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

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

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