关键词:
一阶逻辑
定理证明
人工智能
多元演绎
组合优化
摘要:
一阶逻辑自动定理证明是人工智能领域重要的研究分支,其中子句选择策略对于提升定理证明能力具有重要作用。多元矛盾体分离演绎具有许多良好的演绎特性。为更好地指导多元演绎中的子句选择,提出了一种策略动态组合优化多元演绎方法,通过将子句文字数大小和函数项深度进行动态组合并迭代优化,在充分发掘现有多元演绎启发式策略的同时,提升策略应对不同问题的自适应性,实现多元演绎中的子句高效选择。基于该方法给出了相应的算法实现,根据不同问题的演绎过程动态调整子句的选择策略,提升了多元演绎的定理证明能力。同时,将该算法应用于国际先进的证明器Eprover 2.6,形成了改进的证明器SDCO_E,进一步通过2组实验评估SDCO_E的性能。实验1用2021—2023年国际一阶逻辑自动定理证明器竞赛组的共1500个问题进行测试,结果表明,SDCO_E比Eprover 2.6多证明了35个问题,证明定理总数增加了3.06%;实验2用TPTP库中难度系数为1的问题进行测试,结果表明,SDCO_E能证明其他证明器无法证明的6个数论与集合论领域的问题。实验结果表明,策略动态组合优化多元演绎算法能有效应用于一阶逻辑自动定理证明。