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

Authors

Jian Zhong^{1, 2, *,} , Yang Xu², Feng Cao^{1, 2,}

¹School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China

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

^*Corresponding author. Email: 77367632@qq.com

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)

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  -