矛盾体分离单元结果演绎方法及应用  

A contradiction separation unit resulting deduction method and its application

作　　者：曹锋[1] 谢燏 易见兵[1] 李俊 CAO Feng;XIE Yu;YI Jian-bing;LI Jun(School of Information Engineering,Jiangxi University of Science and Technology,Ganzhou 341000,China)

机构地区：[1]江西理工大学信息工程学院,江西赣州341000

出　　处：《计算机工程与科学》2024年第12期2252-2260,共9页Computer Engineering & Science

基　　金：国家自然科学基金(62366017,62066018);江西省教育厅项目(GJJ200818,GJJ210828);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金(205200100060)。

摘　　要：一阶逻辑自动定理证明是人工智能领域重要的研究内容。为提高单元结果归结演绎效率,提出了一种新的基于多元、动态、协同的单元结果演绎方法,称为矛盾体分离单元结果演绎方法,并详细地给出了其演绎定义、演绎方法、演绎的优势分析及算法实现;提出的演绎方法允许多个子句同时参与演绎,且允许多个非单元子句参与1次单元结果演绎,能较好地处理长子句;提出的演绎算法能使用策略选定较优的子句和动态设定变元合一的复杂度,并通过回溯机制优化搜索的演绎路径。以近2年国际一阶逻辑自动定理证明器竞赛例(分别为500个)和TPTP问题库中难度系数为1的问题作为测试对象,加入了矛盾体分离单元结果演绎算法的Eprover和原始Eprover相比分别多证明了10个定理,分别能证明Eprover无法证明的17个定理和13个定理,能证明出9个其他所有证明器都无法证明难度系数为1的定理。实验结果表明,提出的矛盾体分离单元结果演绎方法能有效提高一阶逻辑自动定理证明的效率。First-order logic automated theorem proving is an important branch in artificial intelligence.In order to improve the deduction efficiency of unit resulting resolution,a new unit resulting deduction method is proposed based on multi-clause,dynamic and synergized deduction,named contradiction separation unit resulting deduction method.Its definition,deduction method,deduction advantage analysis and algorithm implementation are given in detail.The proposed deduction method allows two or more clauses involved in each deduction steps,and allows multiple non-unit clauses to participate in one unit resulting deduction,and it can better handle the long clauses.The proposed deduction algorithm can select optimal clause under the strategy and dynamically set the variable unification complexity,and optimize the deduction search path by backtracking mechanism.Taking the last two years international prover competition problems(The total number is 500 respectively)and the most difficult problems with a rating of 1 from the TPTP benchmark database as the test object,the Eprover with the proposed contradiction separation unit resulting deduction algorithm can solve 10 theorems and 10 theorems more than the original Eprover respectively.It can solve 17 theorems and 13 theorems respectively that original Eprover cannot solve,and can solve 9 theorems with a rating of 1 that cannot be solved by all other provers.The experimental results show that the proposed contradiction separation unit resulting deduction method can be effectively applied to the first-order logic automated theorem proving.

关 键 词：一阶逻辑 自动定理证明 人工智能 单元结果归结 矛盾体分离规则 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]