一种基于子句稳定度的多元动态演绎算法及应用  

A Multi-clause Dynamic Deduction Algorithm Based on Clause Stability and Its Application

作　　者：曹锋[1] 王家帆 易见兵[1] 李俊 CAO Feng;WANG Jiafan;YI Jianbing;LI Jun(School of Information Engineering,Jiangxi University of Science and Technology,Ganzhou Jiangxi 341000,China)

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

出　　处：《广西师范大学学报（自然科学版）》2024年第6期164-176,共13页Journal of Guangxi Normal University:Natural Science Edition

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

摘　　要：一阶逻辑自动定理证明是人工智能领域的核心基础。启发式策略在提升一阶逻辑自动定理证明器方面备受关注,其中根据子句属性选择较优子句参与演绎为重要的研究内容。基于矛盾体分离规则,将子句中的文字分为构建标准矛盾体的文字和构建矛盾体分离式的文字,通过分析变元项、函数项、基项之间的联系与差异,本文提出一种基于稳定度的子句评估方法,其核心思想是通过所含项的组成部分度量子句参与演绎的稳定程度;同时提出一种基于子句稳定度的多元动态演绎算法(clause stability algorithm,CFA),旨在搜索当前演绎过程中的较优路径;将提出的CFA算法应用于国际著名证明器Prover9(CFA_P证明器)和国际顶尖证明器Eprover2.6(CFA_E证明器),使用CFA_P和CFA_E对国际CASC-26 FOF组竞赛例进行测试,相比原始Prover9和原始Eprover2.6,CFA_P多证明119个定理、CFA_E多证明11个定理;在证明相同定理总数的情况下,CFA_P缩短了证明时间14.76 s、CFA_E则缩短了2.54 s;针对Eprover2.6未证明的94个定理进行单独测试,CFA_E能证明27个定理,占定理总数的28.7%。实验表明,CFA算法是有效的,其在优化演绎路径方面具有良好作用,能提高一阶逻辑自动定理证明器的性能。The first-order logic automated theorem proving is the core foundation of artificial intelligence.Heuristic strategies have attracted much attention in improving first-order logic automated theorem provers,and selecting effective clauses based on clause properties to participate in deduction is an important research topic.Based on the standard contradiction separation rule,the literals in clauses are divided into two parts,which are constructing standard contradictory text and constructing contradictory separation text.By analyzing the relationship and differences between variables,functions,and constants,a stability based on clause measurement method is proposed,and its core idea is to evaluate the stability of clause participating in deduction through the components of contained term.A multi-clause dynamic deduction algorithm(CFA,clause stability algorithm)is proposed based on clause stability,aiming to search for optimal paths during the current deduction process.This newly-built CFA algorithm is applied to the internationally well-known prover Prover9 and top prover Eprover2.6,and two new provers CFA_P and CFA_E are formed,respectively.The international competition problems of CASC-26(FOF division)is tested on CFA_P and CFA_E.CFA_P can solve 119 theorems more than the original Prover9,and CFA_E outperforms Eprover2.6,solving 11 theorems more than the original Eprover2.6,and the average proof time of theorems of CFA_P and CFA_E is reduced by 14.76 s and 2.54 s,respectively with the same total number of solved theorems.Focusing on the 94 theorems unsolved by Eprover2.6,CFA_E solves 27 theorems which accounts for 28.7%in the total.The experimental results demonstrate the effectiveness of the CFA algorithm,which has good performance in optimizing deduction paths and can enhance the performance of first-order logic automated theorem prover.

关 键 词：一阶逻辑 定理证明 人工智能 启发式策略 多元动态演绎 

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