An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capability

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.