Multi-clause dynamic deduction algorithm based on clause adequacy evaluation and its application

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． © 2024 Huazhong University of Science and Technology. All rights reserved.