广西师范大学学报（自然科学版）2026，Vol.44Issue(4)：107-120,14.DOI:10.16088/j.issn.1001-6600.2025120301
基于多属性决策的矛盾体分离式评估方法
Evaluation of contradiction separation clause based on multi-criteria decision making
摘要
Abstract
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.关键词
多元演绎/矛盾体分离规则/定理证明器/子句选择策略/一阶逻辑Key words
multi-clause deduction/contradiction separation rule/theorem prover/clause selection strategies/first-order logic分类
信息技术与安全科学引用本文复制引用
曹锋,吴澍康,朱伟臻,易见兵..基于多属性决策的矛盾体分离式评估方法[J].广西师范大学学报（自然科学版）,2026,44(4):107-120,14.基金项目
国家自然科学基金(62366017,62066018) （62366017,62066018）
江西省教育厅项目(GJJ200818,GJJ210828) （GJJ200818,GJJ210828）
江西理工大学博士启动基金(205200100060) （205200100060）
