A contradiction separation unit resulting deduction method and its application
First-order logic automated theorem proving is an important branch in artificial intelli-gence.In order to improve the deduction efficiency of unit resulting resolution,a new unit resulting de-duction method is proposed based on multi-clause,dynamic and synergized deduction,named contradic-tion 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 origi-nal 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 deduc-tion method can be effectively applied to the first-order logic automated theorem proving.
万方数据
维普
