[發明專利]一階邏輯中基于矛盾體分離式的逆向并行演繹推理方法在審
| 申請號： | 201710335863.8 | 申請日： | 2017-05-12 |
| 公開（公告）號： | CN108875949A | 公開（公告）日： | 2018-11-23 |
| 發明（設計）人： | 徐揚;陳樹偉;劉軍;鐘小梅;何星星 | 申請（專利權）人： | 西南交通大學 |
| 主分類號： | G06N5/04 | 分類號： | G06N5/04 |
| 代理公司： | 成都天嘉專利事務所(普通合伙) 51211 | 代理人： | 蔣斯琪 |
| 地址： | 610031 四川省*** | 國省代碼： | 四川;51 |
| 權利要求書： | 查看更多 | 說明書： | 查看更多 |
| 摘要： | |||
| 搜索關鍵詞： | 矛盾體 一階 并行 判定 并行處理 程序驗證 動態分解 構造矛盾 機器證明 邏輯公式 設定條件 屬性判定 有效指導 可用 | ||
1.一階邏輯中基于矛盾體分離式的逆向并行演繹推理方法，其特征在于包括如下步驟：
(一)構造標準矛盾體并形成矛盾體分離式：對于一階邏輯中的子句集S＝{C1,C2,…,Cm}，其中C1,C2,…,Cm為一階邏輯中的子句；從子句集S中選取k個子句D1,…,Di,…,Dk，對子句Di依次做替換σi，Di做替換后分成兩個部分子句和構造標準矛盾體并形成矛盾體分離式其中，m是子句集S中子句的個數，k是選自子句集S用于構造標準矛盾體的子句個數；m≥2，k≥2；：i＝1，2，…，k；
(二)根據矛盾體分離式判斷演繹推理是否終止：如果步驟(一)所得的矛盾體分離式不是基子句，則返回步驟(一)，否則，如果所得矛盾體分離式為基子句，則判斷子句集的不可滿足性：如果矛盾體分離式為空，則停止，得到結論：子句集S不可滿足；否則，轉到步驟(三)；
(三)基于矛盾體分離式構造逆向演繹子句集：
根據步驟(一)選擇矛盾體分離式R，記其中，yj是一階邏輯中的文字，t是矛盾體分離式中文字的個數，t≥1，j＝1，…，t；用矛盾體分離式R與子句集S協同構造t個新子句集S'，S'＝S∪{yj}，然后轉到步驟(四)；
(四)并行演繹推理：對步驟(三)中得到的t個新子句集S'進行并行演繹推理或者逐個進行演繹推理，分別得到相應的演繹推理結果Rj；
如果得到的Rj都是空子句，則得到結論：子句集S不可滿足；
否則，對子句集S或不是空子句的所有Rj對應的新子句集S'再次進行步驟(一)～(四)的演繹推理，直至得到子句集S不可滿足性的判定結論，或達到設定的條件，則停止演繹推理，給出結論：子句集S屬性無法判定。
2.根據權利要求1所述的一階邏輯中基于矛盾體分離式的逆向并行演繹推理方法，其特征在于：步驟(一)中，從子句集中選取k個子句，其中的子句可重復出現。
3.根據權利要求1所述的一階邏輯中基于矛盾體分離式的逆向并行演繹推理方法，其特征在于：步驟(一)中，對子句Di依次做非空替換σi，或者空替換。
4.根據權利要求1所述的一階邏輯中基于矛盾體分離式的逆向并行演繹推理方法，其特征在于：對于子句集S，稱子句為C1,C2,…,Cm的標準矛盾體分離式，如果：
(1)C1,C2,…,Cm不含相同變元；如含有相同變元，則可通過更名替換使其不含相同變元；
(2)對子句Ci1，其中i1＝1,2,…,m；對子句Ci1做替換σi1并做相同文字的合并得到將分為兩個部分子句與使得：
①與無相同文字，所述可以為空子句，所述不為空子句；
②對于任意的P1,…,Pm中有互補對，稱是一個標準矛盾體；
(3)
該專利技術資料僅供研究查看技術是否侵權等信息，商用須獲得專利權人授權。該專利全部權利屬于西南交通大學，未經西南交通大學許可，擅自商用是侵權行為。如果您想購買此專利、獲得商業授權和技術合作，請聯系【客服】
本文鏈接：http://www.szxzyx.cn/pat/books/201710335863.8/1.html，轉載請聲明來源鉆瓜專利網。
