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

在審

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

本發明公開了一階邏輯中基于矛盾體內部子句的逆向并行演繹推理方法，該方法依次通過：對一階邏輯中的子句集S構造矛盾體并形成矛盾體分離式，根據矛盾體分離式判斷演繹推理是否終止：如果S不可滿足，則停止；否則，抽取標準矛盾體內部子句以得到的t個子句為目標，分別對S進行演繹推理，如果能演繹出這t個子句，則停止演繹，得到結論：S不可滿足；否則，循環如上過程，直至得到S屬性的判定結論或滿足設定條件停止；本發明能動態抽取標準矛盾體內部子句，形成動態逆向演繹目標，實現對邏輯公式集屬性判定的并行處理，有效指導演繹推理，提高基于矛盾體分離的動態自動演繹推理系統的演繹效率；本發明可應用于程序驗證、定理機器證明等領域。

技術領域

本發明屬于基于邏輯的自動演繹推理技術領域，涉及一階邏輯中基于矛盾體內部子句的逆向并行演繹推理方法。

背景技術

邏輯學、數學、系統優化、人工智能、計算機科學等領域大量的科學問題都可形式化為邏輯表示，解決這些問題的本質之一就是對相應邏輯公式屬性(可滿足性或不可滿足性(恒假性))的判定，但因其抽象性、復雜性、規模性，無法人工有效地實現邏輯推理與求解，因而需要借助于計算機自動對其判定。自動推理是將推理過程通過一系列符號而形式化，使計算機自動地按某種規則對這些符號實施一系列演算的過程，它是一種智能化行為。先進的基于邏輯的自動推理理論、方法與系統可為解決這些高度復雜的問題提供嚴謹、快速的邏輯證明科學手段，可使機器類似于人類證明定理一樣自動地、系統地、嚴格地按照邏輯規則推理證明邏輯公式的屬性。這種方法和系統是基本的、必需的、科學的、系統的、普適的工具，也是極其難于構造的工具，可廣泛應用于所有基于邏輯的各應用領域的邏輯問題判定。

如前所述，自動推理用于判定形式化為邏輯公式的實際問題的屬性，因本發明涉及一階邏輯中的一種自動演繹推理方法，這里先介紹一下一階邏輯中的一些相關概念，詳細介紹見書《基于歸結方法的自動推理》第一章與第二章。一階邏輯中有四種基本的形式化符號：常量符號(記為a)、變量符號(記為x)、函數符號(記為f)和謂詞符號(記為P)。常量符號、變量符號、函數符號構成項(記為t)，不含變量符號的項稱為基項。作用在項上的謂詞符號構成原子公式(簡稱原子)，原子P或原子的非(即“否定”)～P稱為文字，如果兩個文字中一個是另外一個的非，則稱它們互補，或稱其為互補對。有限個文字的析取(即文字之間的關系為“或者”的關系)稱為子句，記為C＝P₁∨P₂∨···∨P_k，其中P_i(i＝1,2,…,k)是一個文字。只含有一個文字的子句稱為單文字子句。不含文字的子句稱為空子句，記為不含變量符號的子句稱為基子句。子句也表示其所含所有文字的集合，即C＝{P₁,P₂,···,P_k}，表示m個子句C₁,C₂,…,C_m的笛卡爾積。一個邏輯公式可以化為合取范式，即有限個子句的合取(即子句之間的關系為“并且”的關系)，記為S＝C₁∧···∧C_m。轉化為合取范式的公式也稱為子句集，記為S＝{C₁,C₂,…,C_m}。公式的真假性(一般用0表示假，1表示真)通過語義解釋實現。(語義)解釋通過對公式中所有原子賦以0或者1，再由原子間的邏輯運算(非、析取、合取等)即可得到整個公式的真假性。設空子句的真值恒為“假(0)”。如果一個公式在某一解釋下真值為1，則稱它為可滿足的。如果一個公式在任意解釋下的真值都為0，則稱其為稱為恒假的或不可滿足的。在基于邏輯的演繹推理過程中，經常用到替換，即將子句中的變量符號替換為不同于這些變量符號的項。如果替換后的項均為變量，則稱此替換為更名替換。