基于多属性决策的矛盾体分离式评估方法OA

The multi-clause deduction algorithm is the reasoning core of automated theorem provers based on the contradiction separation rule.It is characterized by multi-clause and dynamic deduction features that differ from binary deduction methods.Currently,clause selection strategy methods are a hotspot in research on multi-clause deduction,effectively optimizing multi-clause deduction paths.However,there is a lack of comprehensive evaluation aimed specifically at the deduction paths themselves.The standard contradiction separation clause evaluation method is a novel multi-clause deduction path evaluation mechanism that can effectively guide the search for multi-clause deduction paths.The multi-criteria decision making method is applied to the evaluation of standard contradiction separation clause.Firstly,the attribute of the contradiction separation clause is measured,objectively weighted using the entropy weight method,and evaluated through a combination of multi-criteria optimization and compromise solutions.Secondly,based on this evaluation method,a multi-clause deduction algorithm is proposed,which can evaluate the standard.Finally,this multi-clause deduction algorithm is applied to the international advanced first-order logic contradiction separation clause while dynamically updating its evaluation criteria.It can avoid searching for invalid paths through a backtracking mechanism,thereby effectively improving the inference ability of multi-clause deduction.The proposed algorithm is implemented in the automated theorem prover Eprover 3.2 and tested on the problems from the last three years of international automated theorem provers competition and TPTP(Thousands of Problems for Theorem Provers)problem library with a rating of 1.Eprover3.2 with the proposed algorithm solves 14,14 and 20 additional theorems compared with the original Eprover3.2 respectively,and it also solves 9 theorems with a rating of 1.The experimental results show that the proposed multi-clause deduction method can be effectively applied to the first-order logic automated theorem proving.