基于长子句演绎能力的多元演绎算法OA

To improve the efficiency of participating in the deduction of long clauses with more literals,the rare attributes of long clauses were defined by measuring their literal structure,and the deduction order was obtained,and a method for the effectively selecting and efficiently participating in multi-clause deduction of long clauses was proposed,which could fully utilize the multi-clause and synergized deduction capability of long clauses.Based on this method,a multi-clause deduction algorithm was proposed,which could fully evaluate the effectiveness of the long clauses participating in deduction and allow long clauses to flexibly participate in the deduction of set conditions through backtracking mechanism,thus achieving the deduction path optimization.The algorithm was applied to the international top first-order logic automated theorem prover Eprover3.1,forming a new prover named LC-Eprover3.1.Taking the last two years international automated theorem provers competition problems(the total number is 500 respectively)and the problems from TPTP problem library with a rating of 1 as test object,results show that LC-Eprover3.1 solves 17 theorems and 10 theorems more than the original Eprover3.1,respectively,and can solve 19 theorems and 14 theorems respectively that the original Eprover3.1 cannot solve,and can solve 7 theorems that cannot be solved by all other provers.Experimental results demonstrated the effectiveness of the multi-clause deduction algorithm based on long clauses deduction capability.