International Journal of Computational Intelligence Systems

Volume 13, Issue 1, 2020, Pages 672 - 680

A Novel Combinational ATP Based on Contradiction Separation for First-Order Logic

Authors
Jian Zhong1, 2, *, ORCID, Yang Xu2, Feng Cao1, 2, ORCID
1School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China
2National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu 610031, China
*Corresponding author. Email: 77367632@qq.com
Corresponding Author
Jian Zhong
Received 7 April 2020, Accepted 15 May 2020, Available Online 12 June 2020.
DOI
10.2991/ijcis.d.200521.001How to use a DOI?
Keywords
First-order logic; Theorem proving; Prover9; Contradiction separation rule; Dynamic multi-clause synergized deduction
Abstract

At present, most of the first-order logic theorem provers use a binary-resolution method, which can effectively solve the general first-order logic problems to a certain extent. However, the cooperative processing ability of this method for multiple clauses is insufficient, and it is easy to cause rapid expansion of clause set in the deductive process. In this paper, we propose a novel first-order logic theorem prover based on the standard contradiction separation (S-CS) rule. This prover can realize the dynamic cooperative deduction of multiple clauses in each deduction process, as well as it can effectively learn and control the deduction process. This paper incorporates the S-CS rule with the well-known prover Prover9, to build a combined system, which effectively integrates the advantages of the two methods, not only improves the binary-resolution prover's ability, but also solves more than 100 problems that cannot be solved by other provers.

Copyright
© 2020 The Authors. Published by Atlantis Press SARL.
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)

Journal
International Journal of Computational Intelligence Systems
Volume-Issue
13 - 1
Pages
672 - 680
Publication Date
2020/06/12
ISSN (Online)
1875-6883
ISSN (Print)
1875-6891
DOI
10.2991/ijcis.d.200521.001How to use a DOI?
Copyright
© 2020 The Authors. Published by Atlantis Press SARL.
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

TY  - JOUR
AU  - Jian Zhong
AU  - Yang Xu
AU  - Feng Cao
PY  - 2020
DA  - 2020/06/12
TI  - A Novel Combinational ATP Based on Contradiction Separation for First-Order Logic
JO  - International Journal of Computational Intelligence Systems
SP  - 672
EP  - 680
VL  - 13
IS  - 1
SN  - 1875-6883
UR  - https://doi.org/10.2991/ijcis.d.200521.001
DO  - 10.2991/ijcis.d.200521.001
ID  - Zhong2020
ER  -