Fully reusing clause deduction algorithm based on standard contradiction separation rule
Information Sciences(2023)
摘要
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.
更多查看译文
关键词
ATP,S-CS,FRC algorithm,SDDA,CADE,CASC,FOF,TPTP,CNF,SC,CSC
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要