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

doi:10.16088/j.issn.1001-6600.2024020302

广西师范大学学报（自然科学版） ›› 2024, Vol. 42 ›› Issue (06) : 164 -176. DOI: 10.16088/j.issn.1001-6600.2024020302

曹锋, 王家帆, 易见兵, 李俊

作者信息 +

Author information +

文章历史 +

PDF

摘要

一阶逻辑自动定理证明是人工智能领域的核心基础。启发式策略在提升一阶逻辑自动定理证明器方面备受关注，其中根据子句属性选择较优子句参与演绎为重要的研究内容。基于矛盾体分离规则，将子句中的文字分为构建标准矛盾体的文字和构建矛盾体分离式的文字，通过分析变元项、函数项、基项之间的联系与差异，本文提出一种基于稳定度的子句评估方法，其核心思想是通过所含项的组成部分度量子句参与演绎的稳定程度；同时提出一种基于子句稳定度的多元动态演绎算法(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算法是有效的，其在优化演绎路径方面具有良好作用，能提高一阶逻辑自动定理证明器的性能。