Multi-clause deduction algorithm based on dynamic combination optimization of strategies and its application(策略动态组合优化多元演绎算法及应用)

Abstract

First-order logic automated theorem proving is an important research branch in the field of artificial intelligence, and the clause selection strategy plays an important role in improving the capability of theorem proving. Multi-clause contradiction separation deduction is recognized as the first proposed multi-clause deduction method, which has many good deduction characteristics. In order to better guide the clause selection in multi-clause deduction, multi-clause deduction method based on dynamic combination optimization of strategies is proposed. This method dynamically combines and iteratively optimizes the number of words and function term depth of clause, fully exploring the existing multi-clause deduction heuristic strategies while improving the adaptability of different problems to strategies, achieving efficient clause selection of multi-clause deduction. Based on this method, we demonstrate corresponding algorithm implementations, which can dynamically adjusts the clause selection strategy according to the deduction process of different problems, thereby improving the theorem proving capability of multi-clause deduction. We applied the algorithm to the international advanced Eprover 2.6, to form an improved SDCO_E prover. The performance of SDCO_E is evaluated by two sets of experiments: Experiment 1 took the international first-order logic automated theorem prover competition problems (1 500 in total) in recent three years as test object, SDCO_E solved 35 problems more than the original Epover 2.6, and the total number of theorem proofs has increased by 3.06%; Experiment 2 took problems with a rating of 1 in the TPTP benchmark as test object, SDCO_E solved 6 problems in the field of Number Theory and Set Theory, which has not been solved by all other provers. The experimental results show that the proposed multi-clause deduction algorithm can be effectively applied to first-order logic automated theorem proving.(一阶逻辑自动定理证明是人工智能领域重要的研究分支，其中子句选择策略对于提升定理证明能力具有重要作用。多元矛盾体分离演绎具有许多良好的演绎特性。为更好地指导多元演绎中的子句选择，提出了一种策略动态组合优化多元演绎方法，通过将子句文字数大小和函数项深度进行动态组合并迭代优化，在充分发掘现有多元演绎启发式策略的同时，提升策略应对不同问题的自适应性，实现多元演绎中的子句高效选择。基于该方法给出了相应的算法实现，根据不同问题的演绎过程动态调整子句的选择策略，提升了多元演绎的定理证明能力。同时，将该算法应用于国际先进的证明器Eprover 2.6，形成了改进的证明器SDCO_E，进一步通过2组实验评估SDCO_E的性能。实验1用2021—2023年国际一阶逻辑自动定理证明器竞赛组的共1 500个问题进行测试，结果表明，SDCO_E比Eprover 2.6多证明了35个问题，证明定理总数增加了3.06%；实验2用TPTP库中难度系数为1的问题进行测试，结果表明，SDCO_E能证明其他证明器无法证明的6个数论与集合论领域的问题。实验结果表明，策略动态组合优化多元演绎算法能有效应用于一阶逻辑自动定理证明。)

Keywords

• first-order logic(一阶逻辑)
• theorem proving(定理证明)
• artificial intelligence(人工智能)
• multi-clause deduction(多元演绎)
• combination optimization(组合优化)