子句充分性评估的多元动态演绎算法及应用  

Multi-clause dynamic deduction algorithm based on clause adequacy evaluation and its application

作　　者：曹锋[1] 潘世成 易见兵[1] 李俊 CAO Feng;PAN Shicheng;YI Jianbing;LI Jun(School of Information Engineering,Jiangxi University of Science and Technology,Ganzhou 341000,Jiangxi China)

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

出　　处：《华中科技大学学报（自然科学版）》2024年第11期153-160,共8页Journal of Huazhong University of Science and Technology(Natural Science Edition)

基　　金：国家自然科学基金资助项目(62066018,62106206)。

摘　　要：为了充分体现子句参与多元动态演绎的灵活性、协同性和充分性,将参与多元演绎的子句划分为主动子句和被动子句,提出一种不同类型的子句充分性评估方法,能较好体现子句的充分性演绎且避免重复路径的搜索.基于该子句评估方法提出一种充分使用子句的多元动态演绎算法,能通过回溯机制搜索较优的演绎路径.将该算法应用于国际顶尖的证明器Eprover中,以2020年和2021年国际一阶逻辑自动定理证明器竞赛例为测试对象,在标准测试时间300 s内,加入了该多元动态演绎算法的Eprover2.4分别比原始Eprover2.4多证明定理11个和9个,能证明Eprover2.4无法证明的定理分别为14个和13个;以定理证明器的数千个问题(TPTP)中等级为1的定理作为测试对象,加入了该多元动态演绎算法的Eprover2.4能有效证明出7个所有证明器都未证明的定理.实验结果表明:所提出的多元动态演绎算法能有效应用于一阶逻辑自动定理证明.To fully reflect the flexibility,synergies,and adequacy of clauses participating in multi-clause dynamic deduction,clauses participating in multi-clause deduction were divided into active clauses and passive clauses,and a different type of clause adequacy evaluation method was proposed,which could effectively reflect clause adequacy deduction and avoid searching for repetitive paths.Based on this clause evaluation method,a multi-clause dynamic deduction algorithm based on full use of clauses was proposed,which could search for optimized deduction paths through backtracking mechanism.The algorithm was applied to the international top prover—Eprover.Taking the 2020 and 2021 international first-order logic automated theorem prover competition problems as test objects,in the standard test time of 300 s,Epover2.4 with the proposed multi-clause dynamic deduction algorithm outperformed the original Epover2.4,which solved 11 theorems and 9 theorems more than the original Epover2.4,respectively,and could solve 14 theorems and 13 theorems respectively that Epover2.4 couldn't solve.Taking problems with a rating of 1 in the thousands of problems for theorem provers(TPTP)as the test object,Eprover2.4 with the proposed multi-clause dynamic deduction algorithm could solve 7 theorems that was not proved by all other provers.Experiment results show that the proposed multi-clause dynamic deduction algorithm can be effectively applied to the first-order logic automated theorem proving.

关 键 词：多元动态演绎 回溯机制 演绎路径 一阶逻辑 自动定理证明器 

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