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

在審

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

1.一種基于矛盾體分離超演繹的自動定理證明方法，應用于自動定理證明系統，其特征在于，包括：

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

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

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

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

2.如權利要求1所述的自動定理證明方法，其特征在于，所述遍歷所述演繹子句集中子句所包含的文字，對不同子句的互補謂詞進行合一，生成矛盾體分離超演繹分離式的步驟，包括：

遍歷所述演繹子句集中子句所包含的文字，通過變元替換校驗文字是否可合一；

若所述核子子句中其它文字可與當前演繹文字合一，則合并所述核子子句中文字，若所述電子子句中其它文字可與當前演繹文字合一，則合并所述電子子句中文字；

將所有有效合一文字加入至標準矛盾體中，并析取參與演繹的子句中未有效合一文字生成矛盾體分離超演繹分離式。

3.如權利要求2所述的自動定理證明方法，其特征在于，所述將所有有效合一文字加入至標準矛盾體中，并析取參與演繹的子句中未有效合一文字生成矛盾體分離超演繹分離式的步驟之前，還包括：

按照預設合一規則評估合一有效性；

其中，當參與演繹的子句合一后為恒真式時，合一無效；

當參與演繹的子句中未參與有效合一的文字總數大于設定的閾值時，合一無效；

當正等詞項出現恒等式時，合一無效。

4.如權利要求1至3中任意一項所述的自動定理證明方法，其特征在于，所述生成矛盾體分離超演繹分離式的步驟之后，還包括：

記錄每一輪矛盾體分離超演繹時參與演繹的子句和生成的矛盾體分離超演繹分離式，生成演繹搜索路徑；

對所述演繹搜索路徑進行輸出；其中，所述演繹搜索路徑用于定理證明過程正確性檢查，或用于定理的輔助證明。

5.一種基于矛盾體分離超演繹的自動定理證明裝置，應用于自動定理證明系統，其特征在于，包括：

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

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

輸出模塊，用于在所述矛盾體分離超演繹分離式為空子句時，輸出定理被證明的判定結果；

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