期刊
INFORMATION SCIENCES
卷 566, 期 -, 页码 281-299出版社
ELSEVIER SCIENCE INC
DOI: 10.1016/j.ins.2021.03.015
关键词
Automated theorem proving; First-order logic; Binary resolution; Standard contradiction separation; S-CS dynamic deduction; ATP systems
资金
- Natural Science Foundation of China [61673320]
- Natural Science Foundation of Jiangxi Province [20181BAB202004]
- The General Research Project of Jiangxi Education Department [GJJ200818]
- The Humanities and Social Sciences Research Project of the Ministry of Education of P. R. China [20XJCZ H016]
This paper introduces a novel dynamic deduction algorithm SDDA based on the S-CS inference rule, and evaluates its application effect on current mainstream ATP systems. Experimental results show that SDDA can improve the problem-solving performance of systems like Vampire and E.
In the past decades, automated theorem proving (ATP) for first-order logic has made good progress, in which binary resolution inference rule plays a crucial role. However, as shown in the latest benchmark library of the ATP system, there are still many practical problems that have not been resolved or cannot be effectively resolved. Recently, in order to overcome the limitations of ATP based on binary resolution inference rules, a novel multi clause dynamic standard contradiction separation (S-CS) inference rule and its automated deduction theory have been proposed. Based on this theory, this paper first clarifies the generality of this S-CS rule by comparing it with some well-known variants of the binary resolution rule, and then focuses on how to design a specific and effective algorithm along with search strategies to realize the S-CS based deductive theory with its implementation. Specifically, the present work proposes a novel S-CS dynamic deduction algorithm (in short SDDA) based on different strategies and summarizes its implementation procedures. In addition, we focus on evaluating whether SDDA, as a novel perspective multi-clause dynamic automatic deduction algorithm, can be applied on top of the current leading ATP system architectures to further improve their performances. Therefore, SDDA is applied to the current leading first-order ATP systems, i.e., Vampire and E, respectively forming two integrated APT systems, denoted as SDDA_V and SDDA_E. Then the capabilities of SDDA_V and SDDA_E are evaluated on the latest benchmark database TPTP, such as the CASC-J9 problems (FOF division) as well as the hard problems with a rating of 1 in the TPTP benchmark database. The experimental results show the effectiveness of SDDA: SDDA_V outperforms Vampire itself, and SDDA_E, outperforms E itself, and the two improved ATP systems have solved a number of hard problems with the rating of 1 in TPTP, that is, some problems in the latest benchmark database TPTP which have not yet been solved by other current first-order ATP systems. CO 2021 Elsevier Inc. All rights reserved.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据