A Novel Conflict Deduction Algorithm Based on Contradiction Separation Inference Rule

Automated reasoning, a significant field within artificial intelligence, has attracted increased attention in recent years due to the rising demand for trustworthy AI. Binary resolution, among other inference rules, is crucial in automated reasoning of first-order logic, including the new conflict resolution method. Conflict resolution processes only two clauses in each deduction step and eliminates a complementary pairs of literals from input clauses. This paper proposes a contradiction separation conflict deduction (CSCD) method based on the contradiction separation rule to address these limitations. This novel resolution methodology, together with its automated reasoning theory and method, handles several clauses in each deduction step to seek for conflicts and generates learnt clauses through synergized deduction. Thus, the approach improves deduction by detecting conflicts more effectively, especially with lengthier input clauses. CSCD and conflict resolution are analyzed in detail, then how to create a practical CSCD algorithm and its implementation is summarized. We tested the CSCD algorithm to solve the CASC-26 problems and also applied it to the current leading ATP system (Eprover). Experimental results show that the CSCD deduction approach improves reasoning capability of conflict deduction method. Additionally, the Eprover with the proposed CSCD algorithm improves its performance and has solved various problems with a rating of 1 from the benchmark database TPTP.