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

在審

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

1.命題邏輯中基于矛盾體分離式的逆向并行演繹推理方法，其特征在于包括如下步驟：

(一)構造矛盾體并形成矛盾體分離式：對于命題邏輯中的子句集S＝{C₁,C₂,…,C_m}，從子句集中選取k個子句，構造矛盾體并形成矛盾體分離式R；其中，C₁,C₂,…,C_m為命題邏輯中的子句；m是子句集S中子句的個數，k是選自子句集S用于構造矛盾體的子句個數；m≥2，k≥2；

(二)利用步驟(一)中得到的矛盾體分離式，判斷子句集的不可滿足性：如果判定子句集不可滿足，則停止判斷，得到結論：子句集S不可滿足；否則，然后轉到步驟(三)；

(三)基于矛盾體分離式構造逆向演繹子句集：根據步驟(一)形成的矛盾體分離式其中y_j是命題邏輯中的文字，t是矛盾體分離式中文字的個數，t≥1，j＝1，…，t；利用矛盾體分離式R與子句集S協同構造t個新子句集S'，S'＝S∪{y_j}，然后轉到步驟(四)；

(四)演繹推理：對步驟(三)中得到的t個新子句集進行并行演繹推理或逐個進行演繹推理，分別得到相應的演繹推理結果R_j：

如果得到的R_j都是空子句，則得到結論：子句集S不可滿足；

否則，對子句集S或不是空子句的R_j對應的新子句集S'再次進行步驟(一)～(四)的演繹推理，直至得到子句集S不可滿足性的判定結論，或達到設定的條件，則停止演繹推理，給出結論：子句集S屬性無法判定。

2.根據權利要求1所述的命題邏輯中基于矛盾體分離式的逆向并行演繹推理方法，其特征在于：步驟(一)中，從子句集中選取k個子句，其中的子句可重復出現。

3.根據權利要求1所述的命題邏輯中基于矛盾體分離式的逆向并行演繹推理方法，其特征在于：

對于命題邏輯中的子句集S＝{C₁,C₂,…,C_m}，

(1)如果對于任意的中有互補對，則稱或子句集S是一個標準矛盾體；

(2)如果不可滿足，則稱或S是一個準矛盾體；

在命題邏輯中，標準矛盾體和準矛盾體是同一概念，簡稱為矛盾體。

4.根據權利要求1所述的命題邏輯中基于矛盾體分離式的逆向并行演繹推理方法，其特征在于：針對命題邏輯中的子句C₁,C₂,…,C_m，稱子句為C₁,C₂,…,C_m的矛盾體分離式，如果：

(1)對子句C_i，其中i＝1,…,m；存在C_i中的兩個部分子句與使得：

①與無相同文字，其中：為非空子句；

②不可滿足；

(2)