Abstract: The first-order logic theorem proving is the core foundation of artificial intelligence,it has great academic significance to study the theory and efficient algorithm implementation for first-order logic automated theorem provers.The current provers adopt clause set preprocessing approaches to reduce clause set scale,then apply inference rules to prove theorems.The existing clause set preprocessing method used in provers is generally only from the perspective of the semantic relevance to axioms and conjecture,and it can't reflect the deduction between clauses well from the complementary pairs of literals point of view.In order to describe the relationship between clauses from the perspective of deduction,the definition of goal deduction distance and the calculation method are proposed,and a first-order logic clause set preprocessing method is presented based on the proposed goal deduction distance.Firstly,the original clause set is applied with redundant clause simplification and pure literal deletion rule.Then,taking the goal clauses into consideration,the literal goal deduction distance and the clause goal deduction distance are calculated,and finally further clause set preprocessing is realized by the setting threshold of clause deduction distance.We implement the proposed clause set preprocessing method in Vampire that is the winner of the 2017 CADE ATP System Competition (CASC-26) FOF division,and apply it to solve the CASC-26 problem.Within the standard 300 seconds,the top prover Vampire4.1 with the proposed clause set preprocessing method outperforms Vampire4.1 by solving 4 theorems more than Vampire4.1,and 10 out of the 74 problems unsolved by Vampire4.1,accounting for 13.5% of the total.The proposed clause set preprocessing method has affected 77.2% of the solved theorems,and the largest reduction proportion is 51.7%.Experimental results show that the proposed first-order logic clause set preprocessing method is an effective method,which can effectively reduce the clause set scale and improve the ability of first-order logic automated theorem prover.

Key words: Artificial intelligence, Clause set preprocessing, Deduction distance, First-order logic, Redundant clause