浙江大学学报（理学版）2024，Vol.51Issue(6)：732-739,8.DOI:10.3785/j.issn.1008-9497.2024.06.009
策略动态组合优化多元演绎算法及应用
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.关键词
一阶逻辑/定理证明/人工智能/多元演绎/组合优化Key words
first-order logic/theorem proving/artificial intelligence/multi-clause deduction/combination optimization分类
信息技术与安全科学引用本文复制引用
郭海林,曹锋,易见兵,李俊,吴贯锋..策略动态组合优化多元演绎算法及应用[J].浙江大学学报（理学版）,2024,51(6):732-739,8.基金项目
国家自然科学基金资助项目(62366017,62066018,62106206) （62366017,62066018,62106206）
江西省科技厅项目(20212ACB202003) （20212ACB202003）
江西省教育厅项目(GJJ200818,GJJ180482) （GJJ200818,GJJ180482）
江西理工大学博士启动基金(205200100060). （205200100060）
