CSE - A Automated Theorem Prover Based on Standard Contradiction Separation Dynamic Deduction

Abstract Contradiction Separation Extension (CSE in short), an automated theorem prover for first-order logic without equality, which is based on a novel standard contradiction separation (S-CS) inference rule. Different from binary resolution or its refinements, the biggest difference and characteristic of S-CS rule is that each resolution step can handle multiple (two or more) clauses for synergized deduction. This paper mainly describes problem format conversion, clause set preprocessing, deduction framework, distinctive heuristic strategies, S-CS dynamic inference mechanism in CSE. CSE is evaluated through benchmarks and the deduction characteristics of this multi-clause dynamic deduction are demonstrated, e.g., FOF division problems of CASC-26, CASC-J9. In addition, the CASC-J9 is also tested by combined systems, which combine CSE and other prover (Prover9, Eprover, Vampire), and the combined systems is applied to test on the hard problems with rating of 1. Experimental results show the CSE shows a competitive performance and can play a role in first-order logic automated theorem proving.