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 language | English |
---|---|
Pages (from-to) | 337-356 |
Number of pages | 20 |
Journal | Information Sciences |
Volume | 622 |
Early online date | 5 Dec 2022 |
DOIs | |
Publication status | Published (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