Automated theorem prover (ATP) for first-order logic (FOL), as a significant inference engine, is one of the hot research areas in the field of knowledge representation and automated reasoning. E prover, as one of the leading ATPs, has made a significant contribution to the development of theorem provers for FOL, particularly equality handling, after more than two decades of development. However, there are still a large number of problems in the TPTP problem library, the benchmark problem library for ATPs, that E has yet to solve. The standard contradiction separation (S-CS) rule is an inference method introduced recently that can handle multiple clauses in a synergized way and has a few distinctive features which complements to the calculus of E. Binary clauses, on the other hand, are widely utilized in the automated deduction process for FOL because they have a minimal number of literals (typically only two literals), few symbols, and high manipulability. As a result, it is feasible to improve a prover's deduction capability by reusing binary clause. In this paper, a binary clause reusing algorithm based on the S-CS rule is firstly proposed, which is then incorporated into E with the objective to enhance E’s performance, resulting in an extended E prover. According to experimental findings, the performance of the extended E prover not only outperforms E itself in a variety of aspects, but also solves 18 problems with rating of 1 in the TPTP library, meaning that none of the existing ATPs are able to resolve them.
|Number of pages||13|
|Early online date||23 Dec 2022|
|Publication status||Published (in print/issue) - 15 Feb 2023|
Bibliographical noteFunding Information:
This work is supported by the National Natural Science Foundation of China (Grant Nos. 61976130 , 62106206 ), and the General Research Project of Jiangxi Education Department (Grant No. GJJ200818 ).
© 2022 Elsevier B.V.
- Automated reasoning
- Automated theorem prover
- E prover
- First-order logic
- Knowledge representation
- Standard contradiction rule