[發明專利]一階邏輯中基于矛盾體內部子句的逆向并行演繹推理方法

在審

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

1.一階邏輯中基于矛盾體內部子句的逆向并行演繹推理方法，其特征在于包括如下步驟：

(一)構造標準矛盾體并形成矛盾體分離式：對于一階邏輯中的子句集S＝{C₁,C₂,…,C_m}，其中C₁,C₂,…,C_m為一階邏輯中的子句；從子句集S中選取k個子句D₁，…，D_k，對子句D_i依次做替換σ_i，替換后得到子句將子句分成兩個部分子句和構造標準矛盾體并形成矛盾體分離式m是子句集S中子句的個數，k是選自子句集S用于構造標準矛盾體的子句個數；m≥2，k≥2；

(二)根據矛盾體分離式判斷演繹推理是否終止：利用步驟(一)中得到的矛盾體分離式，判斷子句集的不可滿足性：如果矛盾體分離式為空，則停止，得到結論：子句集S不可滿足；否則，轉到步驟(三)；

(三)抽取標準矛盾體內部子句：根據步驟(一)中所構造的標準矛盾體及矛盾體分離式，從替換后的子句中選取不為空的子句；不為空的子句個數為t個，記為抽取這些子句對應的標準矛盾體內部子句然后轉到步驟(四)；其中：t≥1；i＝1，…，k；j＝1，…，t；

(四)并行演繹推理：以步驟(三)中得到的t個標準矛盾體內部子句為目標，分別對子句集S進行并行演繹推理或逐個進行演繹推理；

如果相應的演繹推理結果分別為這t個子句則得到結論：子句集S不可滿足；

否則，重復步驟(一)～(四)或用另外的演繹推理方法，進行下一輪演繹推理，直至得到子句集S不可滿足性的判定結論，或達到設定的條件，則停止演繹推理，給出結論：子句集S屬性無法判定。

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

3.根據權利要求1所述的一階邏輯中基于矛盾體內部子句的逆向并行演繹推理方法，其特征在于：步驟(一)中，對子句D_i依次做非空替換σ_i，或者空替換。

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

(1)C₁,C₂,…,C_m不含相同變元；如含有相同變元，則可通過更名替換使其不含相同變元；

(2)對子句C_i1，其中i1＝1,2,…,m；對子句C_i1做替換σ_i1并做相同文字的合并得到將分為兩個部分子句與使得：

①與無相同文字，所述不為空子句；

②對于任意的P₁,…,P_m中有互補對，稱是一個標準矛盾體；

(3)