矛盾体分离超演绎方法及应用  

Contradiction separation super-deduction method and application

作　　者：曹锋[1] 杨小玲 易见兵[1] 李俊 CAO Feng;YANG Xiaoling;YI Jianbing;LI Jun(School of Information Engineering,Jiangxi University of Science and Technology,Ganzhou Jiangxi 341000,China)

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

出　　处：《计算机应用》2024年第10期3074-3080,共7页journal of Computer Applications

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

摘　　要：作为当前自动定理证明器中常用的推理机制,传统基于二元演绎超归结方法的推理过程限定每次有且只有2个子句参与演绎,这种分离的演绎步骤导致演绎缺失导向性和预判性,演绎效率有待提升。为了提升演绎效率,在理论上,针对传统的超归结方法引入多元演绎思想,提出矛盾体分离超演绎定义和方法,它具有多元性、动态性和导向性的演绎特性;在算法实现中,考虑子句参与演绎具有多元和协同特性,并灵活设定演绎的条件,提出一种具有回溯机制的矛盾体分离超演绎算法。将所提算法应用于Eprover3.1证明器,以国际自动定理证明器2023年竞赛例和TPTP(Thousands of Problems for Theorem Provers)问题库中难度系数为1的问题作为测试对象,在300 s内,应用所提算法的Eprover3.1证明器比原始Eprover3.1多证明了15个定理;当测试相同数量的定理时,所提算法的平均证明时间缩减了1.326 s,能够证明7个难度系数为1的定理。测试结果表明,所提算法能有效地应用于一阶逻辑自动定理证明,提升自动定理证明器的证明能力和效率。As a common inference mechanism in the current automated theorem prover,the traditional hyper-resolution method based on binary deduction is limited to only two clauses involved in each deduction step.The separated deduction steps lead to the lack of guidance and prediction of the binary chain deduction,and its deduction efficiency needs to be improved.To improve the efficiency of deduction,in theory,the idea of multi-clause deduction was introduced into the traditional method of super-resolution,the definition and method of the contradiction separation super-deduction were proposed,which had the deduction characteristics of multi-clause,dynamics and guidance.In the implementation of the algorithm,considering that the clause participation in deduction had multi-clause and synergized characteristics,and flexibly setting the deduction conditions,a contradiction separation super-deduction algorithm with backtracking mechanism was proposed.The proposed algorithm was applied to Eprover3.1 prover,taking the International Automated Theorem Prover Competition 2023 and the most difficult problems with a difficulty rating of 1 in the TPTP(Thousands of Problems for Theorem Provers)benchmark database as the test objects.Within 300 s,the Eprover3.1 prover with the proposed algorithm solved 15 theorems more than the original Eprover3.1 prover,and the average proof time was reduced by 1.326 s with the same total number of solved theorems,and 7 theorems with the rating of 1 could be solved.The test results show that the proposed algorithm can be effectively applied to automated theorem proving in first-order logic,improving the proof capability and efficiency of automated theorem prover.

关 键 词：定理证明器 二元演绎 超归结 多元演绎 矛盾体分离 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]