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

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.

Keywords

• First-order logic
• Theorem proving
• Prover9
• Contradiction separation rule
• Dynamic multi-clause synergized deduction