华中科技大学学报（自然科学版）2024，Vol.52Issue(11)：153-160,8.DOI:10.13245/j.hust.240468
子句充分性评估的多元动态演绎算法及应用
Multi-clause dynamic deduction algorithm based on clause adequacy evaluation and its application
摘要
Abstract
To fully reflect the flexibility,synergies,and adequacy of clauses participating in multi-clause dynamic deduction,clauses participating in multi-clause deduction were divided into active clauses and passive clauses,and a different type of clause adequacy evaluation method was proposed,which could effectively reflect clause adequacy deduction and avoid searching for repetitive paths.Based on this clause evaluation method,a multi-clause dynamic deduction algorithm based on full use of clauses was proposed,which could search for optimized deduction paths through backtracking mechanism.The algorithm was applied to the international top prover—Eprover.Taking the 2020 and 2021 international first-order logic automated theorem prover competition problems as test objects,in the standard test time of 300 s,Epover2.4 with the proposed multi-clause dynamic deduction algorithm outperformed the original Epover2.4,which solved 11 theorems and 9 theorems more than the original Epover2.4,respectively,and could solve 14 theorems and 13 theorems respectively that Epover2.4 couldn't solve.Taking problems with a rating of 1 in the thousands of problems for theorem provers(TPTP)as the test object,Eprover2.4 with the proposed multi-clause dynamic deduction algorithm could solve 7 theorems that was not proved by all other provers.Experiment results show that the proposed multi-clause dynamic deduction algorithm can be effectively applied to the first-order logic automated theorem proving.关键词
多元动态演绎/回溯机制/演绎路径/一阶逻辑/自动定理证明器Key words
multi-clause dynamic deduction/backtracking mechanism/deduction path/first-order logic/automated theorem prover分类
信息技术与安全科学引用本文复制引用
曹锋,潘世成,易见兵,李俊..子句充分性评估的多元动态演绎算法及应用[J].华中科技大学学报（自然科学版）,2024,52(11):153-160,8.基金项目
国家自然科学基金资助项目(62066018,62106206). （62066018,62106206）
