[發明專利]命題邏輯中基于矛盾體分離式的逆向并行演繹推理方法

在審

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

本發明公開了命題邏輯中基于矛盾體分離式的逆向并行演繹推理方法，該方法步驟為：對命題邏輯中子句集S構造矛盾體并形成矛盾體分離式，根據矛盾體分離式判斷S的不可滿足性：如果判定S不可滿足則停止，否則，基于矛盾體分離式構造逆向演繹子句集，得到t個新子句集并進行演繹推理，如果對t個新子句集的演繹結果都是空子句，則S不可滿足，否則循環前述步驟，直至得到S屬性的判定結論或滿足設定條件停止；本發明能動態分解矛盾體分離式，形成動態逆向演繹目標，有效指導下一步演繹推理，并對分解后的邏輯公式集屬性判定進行并行處理，有效提高基于矛盾體分離的動態自動演繹推理系統的演繹效率；本發明可用于程序驗證、定理機器證明等領域。

技術領域

本發明屬于基于邏輯的自動演繹推理技術領域，涉及命題邏輯中基于矛盾體分離式的逆向并行演繹推理方法。

背景技術

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

如前所述，自動推理用于判定形式化為邏輯公式的實際問題的屬性。對于命題邏輯，其中最基本的公式為原子，原子x或原子的非(即“否定”)～x稱為文字，如果兩個文字中一個是另外一個的非，則稱它們互補，或稱其為互補對。有限個文字的析取(即文字之間的關系為“或者”的關系)稱為子句，記為C＝x₁∨x₂∨···∨x_k，其中x_i1(i1＝1,2,…,k)是一個文字。只含有一個文字的子句稱為單文字子句。不含文字的子句稱為空子句，記為子句也表示其所含所有文字的集合，即C＝{x₁,x₂,···,x_k}，表示m個子句C₁,C₂,…,C_m的笛卡爾積。一個邏輯公式可以化為合取范式，即有限個子句的合取(即子句之間的關系為“并且”的關系)，記為S＝C₁∧···∧C_m。轉化為合取范式的公式也稱為子句集，記為S＝{C₁,C₂,…,C_m}.公式的真假性(一般用0表示假，1表示真)通過語義解釋實現。(語義)解釋通過對公式中所有原子賦以0或者1，再由原子間的邏輯運算(非、析取、合取等)即可得到整個公式的真假性。設空子句的真值恒為“假(0)”。如果一個公式在某一解釋下真值為1，則稱它為可滿足的。如果一個公式在任意解釋下的真值都為0，則稱其為稱為恒假的或不可滿足的。公式可滿足的情況下，可從它的每個子句中至少找到一個均賦值為1的文字，這組文字稱為該公式或子句集的可滿足例。相關概念的詳細介紹見書《基于歸結方法的自動推理》第一章與第二章。