Fully reusing clause deduction algorithm based on standard contradiction separation rule

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

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)
14 Downloads (Pure)


An automated theorem proving (ATP) system's capacity for reasoning is significantly influenced by the inference rules it uses. The recently introduced standard contradiction separation (S-CS) inference rule extends binary resolution to a multi-clause, dynamic, contradiction separation inference mechanism. The S-CS rule is used in the present work to provide a framework for fully clause reusing deductions. Accordingly, a fully reusing clause deduction algorithm (called the FRC algorithm) is built. The FRC algorithm is then incorporated as an algorithm module into the architecture of a top ATP, Vampire, creating a single integrated ATP system dubbed V_FRC. The objective of this integration is to enhance Vampire's performance while assessing the FRC algorithm's capacity for reasoning. According to experimental findings, V_FRC not only outperforms Vampire in a variety of aspects, but also solves 46 problems in the TPTP benchmark database that have a rating of 1, meaning that none of the existing ATP systems are able to resolve them.
Original languageEnglish
Pages (from-to)337-356
Number of pages20
JournalInformation Sciences
Early online date5 Dec 2022
Publication statusPublished (in print/issue) - 30 Apr 2023

Bibliographical note

Funding Information:
This paper is supported by the National Natural Science Foundation of China (Grant Nos. 61976130, 62106206), the General Research Project of Jiangxi Education Department (Grant No. GJJ200818).

Publisher Copyright:
© 2022 Elsevier Inc.


  • Theorem proving
  • ATP system
  • Inference rule
  • Deduction algorithm
  • Standard contradiction
  • S-CS rule
  • Vampire


Dive into the research topics of 'Fully reusing clause deduction algorithm based on standard contradiction separation rule'. Together they form a unique fingerprint.

Cite this