Multilayer inverse dynamic deduction algorithm of standard contradiction separation rule based on parallel mechanism

The standard contradiction separation (S-CS) rule is a new inference rule recently proposed in the field of automated reasoning, which is characterized by dynamism, robustness, and collaborative deduction of multiple clauses. According to the above characteristics, to further utilize the inference ability of the S-CS rule, we propose an inverse and parallel algorithms to extend and enhance S-CS rule. Specifically, a multi-layer inverse and parallel deduction algorithm (in short MIP) is built. This algorithm transforms the first-order logic clause set into multiple clause sets, which are then recursively and iteratively deduced in parallel such that whenever a clause set is unsatisfiable, the original clause set is unsatisfiable. The main advantages of this algorithm are inverse deduction, parallel deduction, and depth (multi-layer) deduction. In order to improve the performance of automated theorem prover, we embed this algorithm into the current top automated theorem provers Vampire and E to form the new provers MIP_V and MIP_E. Then we test MIP_V with the problems from the international competition (CASC) for automated theorem provers, and test MIP_E and MIP_V with the hardest problem of rating = 1 from the benchmark library TPTP. The experimental results show that MIP_V (MIP_E) has a better performance than Vampire (E), and MIP_V and MIP_E can solve 66 problems with rating = 1.