A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof Search

Feng Cao; Yang Xu; Shuwei Chen; Jian Zhong; Guanfeng Wu

doi:10.2991/ijcis.d.191022.002

<Previous Article In Issue

Next Article In Issue>

Volume 12, Issue 2, 2019, Pages 1245 - 1254

A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof Search

Authors

Feng Cao¹^{, 2}^{, *}, Yang Xu²^{, 3}, Shuwei Chen²^{, 3}^{, *}, Jian Zhong¹^{, 2}, Guanfeng Wu²^{, 3}

¹School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, Sichuan, P.R. China

²National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu 610031, Sichuan, P.R. China

³School of Mathematics, Southwest Jiaotong University, Chengdu 610031, Sichuan, P.R. China

^*Corresponding authors. Email: caofeng@my.swjtu.edu.cn; swchen@swjtu.edu.cn

Corresponding Authors

Feng Cao, Shuwei Chen

Received 19 August 2019, Accepted 15 October 2019, Available Online 12 November 2019.

DOI: 10.2991/ijcis.d.191022.002 How to use a DOI?
Keywords: Automated theorem proving; Binary resolution; Multi-clause inference rule; S-CS rule; Heuristic strategy
Abstract: Most of the advanced first-order logic automated theorem proving (ATP) systems adopt binary resolution methods as the core inference mechanism, where only two clauses are involved and a complementary pair of literals are eliminated during each deduction step. Recently, a novel multi-clause inference rule is introduced along with its soundness and completeness, which is called as standard contradiction separation rule (in short, S-CS rule) and allows multiple (two or more) clauses to be involved in each deduction step. This paper introduces and evaluates the application of S-CS rule in first-order logic ATP. Firstly, it analyzes several deduction methods of S-CS rule. It is then focused on how this multi-clause deduction theory can be achieved through forming a specific and effective algorithm, and finally how it can be applied in the top ATP systems in order to improve their performances. Concretely, two novel multi-clause S-CS dynamic deduction algorithms are proposed based on optimized proof search, including related heuristic strategy, then the application method applied in the state of the art ATP system Eprover (the version of Eprover 2.3) is introduced. Eprover with the proposed multi-clause deduction algorithms are evaluated through the FOF division of the CASC-J9 (in 2018) ATP system competition. Experimental results show that Eprover with the proposed multi-clause deduction algorithms outperform the plain Eprover itself to a certain extent.
Open Access: This is an open access article distributed under the CC BY-NC 4.0 license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)
View full text (HTML)

<Previous Article In Issue

Next Article In Issue>

Journal: International Journal of Computational Intelligence Systems
Volume-Issue: 12 - 2
Pages: 1245 - 1254
Publication Date: 2019/11/12
ISSN (Online): 1875-6883
ISSN (Print): 1875-6891
DOI: 10.2991/ijcis.d.191022.002 How to use a DOI?
Open Access: This is an open access article distributed under the CC BY-NC 4.0 license (http://creativecommons.org/licenses/by-nc/4.0/).

Cite this article

ris enw bib

TY  - JOUR
AU  - Feng Cao
AU  - Yang Xu
AU  - Shuwei Chen
AU  - Jian Zhong
AU  - Guanfeng Wu
PY  - 2019
DA  - 2019/11/12
TI  - A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof Search
JO  - International Journal of Computational Intelligence Systems
SP  - 1245
EP  - 1254
VL  - 12
IS  - 2
SN  - 1875-6883
UR  - https://doi.org/10.2991/ijcis.d.191022.002
DO  - 10.2991/ijcis.d.191022.002
ID  - Cao2019
ER  -

download .riscopy to clipboard