基于子句活跃度和复杂度的多元动态演绎算法及应用

来源：计算机工程与科学杂志2023年第12期北京时间：

作者：林玲瑜, 曹锋, 易见兵, 方旺盛, 李俊, 吴贯锋

单位：1.江西理工大学信息工程学院，江西 赣州341000；2.西南交通大学数学学院，四川 成都 610031

摘要：一阶逻辑自动定理证明是知识表示与自动推理领域重要的研究内容，如何有效选取子句参与演绎是提升自动推理能力和效率的研究热点。基于多元动态演绎良好的演绎特性，通过分析子句的变元项性质和函数项结构，提出了一种子句活跃度和复杂度的度量与计算方法，能很好地对不同项结构的子句进行有效评估；基于该子句评估方法，提出了一种子句充分协同演绎的多元动态演绎算法，能有效优化多元演绎搜索路径。将该多元动态演绎算法应用于国际顶尖证明器Eprover 2.6中，以2021年国际自动推理FOF组竞赛例为测试对象，在标准的300 s测试时间内，加入了多元动态演绎算法的Eprover 2.6相比原始Eprover 2.6多证明定理4个，在证明定理总数相同的条件下，平均证明时间减少了1.12 s；能证明Eprover 2.6未证明定理16个，占未证明定理总数的15.1%。实验结果表明，该多元动态演绎算法是一种有效的推理方法，能在一定程度上提升自动定理的证明能力和时间效率。

关键词：一阶逻辑,定理证明,自动推理,多元动态演绎,子句评估,

基金资助：(1.School of Information Engineering,Jiangxi University of Science and Technology,Ganzhou 341000；2.School of Mathematics,Southwest Jiaotong University,Chengdu 610031，China)