[發明專利]命題邏輯中基于極大子句判定公式屬性的方法

在審

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

1.命題邏輯中基于極大子句判定公式屬性的方法，其特征在于包括如下步驟：對于命題邏輯中的子句集S＝{C₁，…，C_i，…，C_n}，即S＝C₁∧…∧C_i∧…∧C_n，所述C_i為子句，記子句集S中出現的全部命題變元組成的集合V(S)＝{l₁，…，l_q}，其中，l₁，…，l_q是命題變元，q是一個自然數且q≥1，i＝1，2，…，n；

第一步，根據集合V(S)，構造一個關于V(S)的極大子句D(k)；

第二步，將所述D(k)中的全部文字取非，所得的子句為～D(k)＝～p(1)∨…∨～p(j)∨…∨～p(q)；在子句集S中刪去與～D(k)含有相同文字的子句，并將所得子句集記為S₁；

第三步，判定子句集S的屬性：

(1)若則S是可滿足的，方法停止；

(2)若且除D(k)外存在關于V(S)的其他極大子句，則轉第一步；

(3)若且除D(k)外不存在關于V(S)的其他極大子句，則S是不可滿足的，方法停止。

2.根據權利要求1所述命題邏輯中基于極大子句判定公式屬性的方法，其特征在于：所述第一步中，構造的極大子句D(k)＝p(1)∨…∨p(j)∨…∨p(q)，其中，p(j)是一個文字且p(j)＝l_j或～l_j，～l_j是表示l_j的非，j＝1，…，q。

3.根據權利要求1所述命題邏輯中基于極大子句判定公式屬性的方法，其特征在于：所述第二步中，在子句集S中刪去與～D(k)含有相同文字的子句是指刪去S中含文字～p(1)，～p(2)，…，～p(q)的子句。

4.根據權利要求1所述命題邏輯中基于極大子句判定公式屬性的方法，其特征在于：所述第三步中，判定子句集S的屬性的原則如下：

(1)若則S是可滿足的，并給出一個滿足S的解釋I_D，對S中出現的任意命題變元l_j，所述其中j＝1，…，q，方法停止；

(2)若且除D(k)外存在關于V(S)的其他極大子句，則轉第一步；

(3)若且除D(k)外不存在關于V(S)的其他極大子句，則S是不可滿足的，方法停止。

5.根據權利要求1所述命題邏輯中基于極大子句判定公式屬性的方法，其特征在于：對于所述集合V(S)，如果對任意的命題變元l∈V(S)，l與～l為互補對，l與～l有且僅有之一在子句D中出現，且子句D中文字的個數與V(S)所含元素的個數相同，則稱子句D是一個關于集合V(S)的極大子句。