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

4 Citations (Scopus)
36 Downloads (Pure)

Abstract

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
Volume622
Early online date5 Dec 2022
DOIs
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.

Keywords

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

Fingerprint

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