[發(fā)明專利]命題邏輯中基于標準延拓三角形的矛盾體分離演繹推理

在審

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

1.命題邏輯中基于標準延拓三角形的矛盾體分離演繹推理，其特征在于具體包括如下步驟：

(一)對于命題邏輯中的子句集S＝{C₁,C₂,…,C_m}，綜合考慮子句中文字數(shù)及互補文字所處的子句的指標，從子句集中選取k個子句，構(gòu)造基于標準延拓三角形矛盾體；其中，C₁,C₂,…,C_m為命題邏輯中的子句；m是子句集S中子句的個數(shù)，k是選自子句集S用于構(gòu)造矛盾體的子句個數(shù)；m≥2，k≥2；

(二)將步驟(一)中所構(gòu)造的基于標準延拓三角形矛盾體從參與構(gòu)造的k個子句中刪去，并將刪去基于標準延拓三角形矛盾體后的k個子句中的剩余文字按析取關(guān)系組成新的子句，即矛盾體分離式；

(三)利用步驟(二)中得到的矛盾體分離式，判定子句集的屬性：

如果能夠判定子句集不可滿足，則停止，得到結(jié)論：子句集S不可滿足；如果能夠判定子句集是可滿足，則停止，得到結(jié)論：子句集S可滿足，且能給出其可滿足例；

否則，將所得矛盾體分離式加入子句集S，形成新的子句集，然后重復(fù)步驟(一)，接著構(gòu)造并分離基于標準延拓三角形矛盾體，直至得到子句集屬性的判定結(jié)論。

2.根據(jù)權(quán)利要求1所述的命題邏輯中基于標準延拓三角形的矛盾體分離演繹推理，其特征在于：步驟(一)中，可重復(fù)從子句集S中選取k個子句。

3.根據(jù)權(quán)利要求1所述的命題邏輯中基于標準延拓三角形的矛盾體分離演繹推理，其特征在于：步驟(一)中構(gòu)建基于標準延拓三角形矛盾體及步驟(二)中形成矛盾體分離式的具體方法步驟如下：

步驟1，對于子句集S，從子句集S中選擇子句D₁，在子句D₁中選擇文字x₁；利用文字x₁延拓，選擇含文字x₁的補文字～x₁的子句，記為D₂(x₁)；

此時，將子句D₁分成兩部分：子句和子句其中，即表示從D₁中刪去中的文字；

……

步驟i，在子句D_i(x_i-1)中選取文字x_i；然后，將子句D_i(x_i-1)分成兩部分：子句和子句其中，且

……

步驟k-1，在子句D_k-1(x_k-2)中選取文字x_k-1，將子句D_k-1(x_k-2)分成兩部分：子句和子句其中，且然后，選擇含文字x_k的補文字～x_k的子句D_k(x_k-1)；

步驟k，如果無法延拓或不需要再延拓時，則停止延拓；將子句D_k(x_k-1)分成兩部分：子句和子句其中，且

此時，得到基于標準延拓三角形的矛盾體和基于標準延拓三角形的矛盾體分離式其中，

上述過程中，i≥2。

4.根據(jù)權(quán)利要求1所述的命題邏輯中基于標準延拓三角形的矛盾體分離演繹推理，其特征在于判定演繹推理結(jié)果方法為：

(1)當R_s＝φ時，則停止推理，判定子句集S不可滿足；

(2)當R_s≠φ時，

(i)若k＜m，則S＝S∪{R_s}，轉(zhuǎn)到步驟1；

(ii)若k≥m，且基于標準延拓三角形的矛盾體的構(gòu)造中用盡原S中的所有子句，則停止推理，得到結(jié)論：子句集S可滿足，且能給出S的一個可滿足例。