Abstract: First-order logic automated theorem proving is an important branch in artificial intelligence. In order to improve the deduction efficiency of unit resulting resolution, a new unit resulting deduction method is proposed based on multi-clause, dynamic and synergized deduction, named contradiction separation unit resulting deduction method. Its definition, deduction method, deduction advantage analysis and algorithm implementation are given in detail. The proposed deduction method allows two or more clauses involved in each deduction steps, and allows multiple non-unit clauses to participate in one unit resulting deduction, and it can better handle the long clauses. The proposed deduction algorithm can select optimal clause under the strategy and dynamically set the variable unification complexity, and optimize the deduction search path by backtracking mechanism. Taking the last two years international prover competition problems (The total number is 500 respectively) and the most difficult problems with a rating of 1 from the TPTP benchmark database as the test object, the Eprover with the proposed contradiction separation unit resulting deduction algorithm can solve 10 theorems and 10 theorems more than the original Eprover respectively. It can solve 17 theorems and 13 theorems respectively that original Eprover cannot solve, and can solve 9 theorems with a rating of 1 that cannot be solved by all other provers. The experimental results show that the proposed contradiction separation unit resulting deduction method can be effectively applied to the first-order logic automated theorem proving.

Key words: first-order logic, automated theorem proving, artificial intelligence, unit resulting resolution, contradiction separation rule