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

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
JournalInformation Sciences
Volume622
Early online date5 Dec 2022
DOIs
Publication statusPublished online - 5 Dec 2022

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