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