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

Peiyao Liu, Shuwei Chen, J. Liu, Yang Xu, Feng Cao, Guanfeng Wu

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)
13 Downloads (Pure)


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.
Original languageEnglish
Article number110217
Pages (from-to)1-13
Number of pages13
JournalKnowledge-Based Systems
Early online date23 Dec 2022
Publication statusPublished (in print/issue) - 15 Feb 2023

Bibliographical note

Funding 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 ).

Publisher Copyright:
© 2022 Elsevier B.V.


  • Automated reasoning
  • Automated theorem prover
  • E prover
  • First-order logic
  • Knowledge representation
  • Standard contradiction rule


Dive into the research topics of 'An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capability'. Together they form a unique fingerprint.

Cite this