[發明專利]基于超演繹的自動定理證明方法、裝置及存儲介質

在審

• 申請號: 202110646510.6
• 申請日: 2021-06-10
• 公開（公告）號: CN113379050A
• 公開（公告）日: 2021-09-10
• 發明（設計）人: 曹鋒;易見兵;黃江燕;陳鴻坤
• 申請（專利權）人: 江西理工大學
• 主分類號: G06N5/00
• 分類號: G06N5/00;G06N5/04
• 代理公司: 深圳尚業知識產權代理事務所(普通合伙) 44503
• 代理人: 王利彬

本發明公開了一種基于超演繹的自動定理證明方法、裝置及存儲介質，從一階邏輯子句集S選擇包括單個核子子句及多個電子子句的子集構建標準矛盾體，得到矛盾體分離式R。若R為空子句，定理被證明。當R不為空子句時，若R有效且全為正文字，則將R加入到S中，停止本次矛盾體分離超演繹；當R含負文字，則在S中重新選擇子句繼續演繹；若無效，需回退到上一演繹步驟，在S中重新選擇子句繼續演繹；當S遍歷完或滿足定理判定終止條件，結束本次矛盾體分離超演繹。通過本發明的實施，具有每個矛盾體分離演繹只有1個子句含負文字的特點，能有效縮減多元演繹的路徑搜索空間和提升演繹效率，增強了多元演繹推理系統的一階邏輯自動定理證明能力。

技術領域

本發明涉及自動推理技術領域，尤其涉及一種基于超演繹的自動定理證明方法、裝置及存儲介質。

背景技術

自動推理是利用計算機、邏輯推理等技術手段自動地對邏輯公式進行一系列推理，通過這種符號演算形式自動地對邏輯公式屬性進行判定。自動推理是人工智能領域的重要內容，其主要研究內容包括命題邏輯公式求解和一階邏輯定理證明。在實際應用中，很多問題(例如數學定理證明、程序驗證、規則檢查、個性化定制、智能信息處理、知識表示、管理與決策、信息安全和交通運輸等)都可用邏輯系統形式化表示，進而可通過自動推理技術自動化地處理。相比命題邏輯系統，一階邏輯系統通過謂詞符、變元、常元、函數符和邏輯連接詞組成，具有更加豐富的形式化表達能力。因此，一階邏輯系統的自動定理證明方法可廣泛應用于解決一切可用邏輯表示的現實問題。

目前主流的一階邏輯自動定理證明器普遍采用了傳統的超歸結演繹，雖然該鏈式歸結方法也處理多個子句，但本質上仍是二元歸結方法。二元歸結是一種靜態的歸結方式，即每次限定有且只有2個子句進行歸結，消去1組互補對，剩余文字的析取作為演繹歸結式。由于二元歸結是一種靜態的演繹方法，二元歸結方式常含有較多文字數，且不能很好的發揮多子句間的協同關系，降低了演繹效率。

發明內容

本發明實施例的主要目的在于提供一種基于超演繹的自動定理證明方法、裝置及存儲介質，至少能夠解決相關技術中采用傳統超歸結演繹方式進行一階邏輯自動定理證明，所導致的演繹效率較低的問題。

為實現上述目的，本發明實施例第一方面提供了一種基于矛盾體分離超演繹的自動定理證明方法，應用于自動定理證明系統，該方法包括：

步驟A、按照子句是否包含負文字將一階邏輯子句集劃分為電子子句集和核子子句集，并從電子子句集中選取多個子句以及從核子子句集中選取單個子句構建演繹子句集；其中，所述電子子句集中子句只包含正文字，所述核子子句集中子句至少包含1個負文字；

步驟B、遍歷所述演繹子句集中子句所包含的文字，對不同子句的互補謂詞進行合一，生成矛盾體分離超演繹分離式；

步驟C、在所述矛盾體分離超演繹分離式為空子句時，輸出定理被證明的判定結果；

步驟D、在所述矛盾體分離超演繹分離式不為空子句時，若所述矛盾體分離超演繹分離式滿足預設演繹回退條件，則將參與演繹的子句的無效演繹權重加1，繼續選擇所述演繹子句集中的子句進行演繹，并在所述演繹子句集已遍歷完成時返回所述步驟A；若所述矛盾體分離超演繹分離式包含負文字，則返回所述步驟A；若所述矛盾體分離超演繹分離式不包含負文字，則將所述矛盾體分離超演繹分離式添加至所述一階邏輯子句集之中，并返回所述步驟A；其中，在滿足預設系統演繹終止條件時仍未演繹出空子句，則停止演繹，并輸出定理無法證明的判定結果。

為實現上述目的，本發明實施例第二方面提供了一種基于矛盾體分離超演繹的自動定理證明裝置，應用于自動定理證明系統，該裝置包括：

構建模塊，用于按照子句是否包含負文字將一階邏輯子句集劃分為電子子句集和核子子句集，并從電子子句集中選取多個子句以及從核子子句集中選取單個子句構建演繹子句集；其中，所述電子子句集中子句只包含正文字，所述核子子句集中子句至少包含1個負文字；