华中科技大学学报（自然科学版）2026，Vol.54Issue(5)：84-90,7.DOI:10.13245/j.hust.250569
基于长子句演绎能力的多元演绎算法
Multi-clause deduction algorithm based on long clauses deduction capability
摘要
Abstract
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.关键词
多元演绎/回溯机制/演绎路径/一阶逻辑/证明器Key words
multi-clause deduction/backtracking mechanism/deduction path/first-order logic/prover分类
信息技术与安全科学引用本文复制引用
曹锋,谢燏,易见兵,李俊..基于长子句演绎能力的多元演绎算法[J].华中科技大学学报（自然科学版）,2026,54(5):84-90,7.基金项目
国家自然科学基金资助项目(62366017,62066018) （62366017,62066018）
江西省教育厅科技项目(GJJ200818,GJJ210828) （GJJ200818,GJJ210828）
赣州市科技计划资助项目(GZKJ20206030) （GZKJ20206030）
江西理工大学博士启动基金资助项目(205200100060). （205200100060）
