A complementary ratio based clause selection method for contradiction separation dynamic deduction

Automated reasoning is a key research area of Artificial Intelligence (AI) and has attracted much greater attention in recent years due to the demands of trustworthy AI, where binary resolution inference rule based firstorder automated reasoning play a crucial role. Recently, a novel multi-clause dynamic standard contradiction separation (S-CS) inference rule and related automated deduction theory were proposed to overcome the limitations of binary resolution-based automated deduction. Now that strategies for dynamic clause selection are essential for S-CS based automated deduction, in the present work, a class of novel clause selection strategies, along with the corresponding novel complementary ratio based dynamic S-CS automated deduction algorithm (called CRA), are proposed. Furthermore, we are interested in determining whether CRA may be deployed on top of the current best first-order automated reasoning system designs to increase their performance. As a result, CRA is applied to the current leading systems, Vampire and E, resulting in two integrated automatic reasoning systems, CRA_Vampire and CRA_E. Experiment results demonstrate that CRA can improve E and Vampire in CASC 2020-2022 competitions. The new integrated automated reasoning systems can resolve 44 problems with rating of 1, meaning they are intractable by other existing first-order automated systems.