Fully reusing clause deduction algorithm based on standard contradiction separation rule

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.(c) 2022 Elsevier Inc. All rights reserved.

Automated summary

The choice of inference rules significantly affects the reasoning capacity of an automated theorem proving system. The standard contradiction separation (S-CS) rule extends binary resolution to a dynamic, multi-clause, contradiction separation inference mechanism. In this study, the S-CS rule is used to develop a fully reusing clause deduction algorithm (FRC algorithm), which is integrated into the architecture of a top ATP system Vampire, creating a single integrated ATP system called V_FRC. Experimental findings show that V_FRC outperforms Vampire in various aspects and successfully solves 46 rating 1 problems in the TPTP benchmark database that cannot be resolved by existing ATP systems.