华中科技大学学报（自然科学版）2025，Vol.53Issue(5)：157-163,7.DOI:10.13245/j.hust.250191
基于子句正负文字的多元演绎算法
Multi-clause deduction algorithm based on positive and negative literals in clauses
摘要
Abstract
A multi-clause deduction method based on positive and negative literals in clauses was proposed by classifying the positive and negative attributes of participating literals,leveraging the advantageous characteristics of multi-clause deduction.The deduction order of clauses was determined through the attributes of the main literals,resulting in effective literal elimination and optimized multi-clause deduction paths.A multi-clause deduction algorithm was developed based on positive and negative literals in clauses,which was integrated with contradiction separation clause evaluation and a backtracking mechanism.This approach was designed to allow literals to flexibly participate in the deduction of set conditions under passive constraints,thereby enhancing the efficiency of multi-clause deduction.The proposed algorithm was implemented in the internationally advanced first-order logic automated theorem prover-Eprover2.6.When tested on the 2022 and 2023 international competition problems under a 300 s time limit,the enhanced Eprover2.6 was observed to solve 18 and 17 additional theorems respectively compared to the original prover,while the average proof time was reduced by 6.485 s and 5.092 s for theorems with identical total solved counts.Furthermore,19 and 18 theorems previously unsolved by Eprover2.6 were successfully resolved,accounting for 15.70%and 14.63%of Eprover2.6's original unsolved theorems.When evaluated on TPTP(thousands of problems for theorem provers)problem library's rating of 1 problems,10 theorems unsolvable by all other provers were demonstrated to be solvable by this method.Experiment results show that the proposed multi-clause deduction framework can significantly improve both capability and efficiency in first-order logic automated theorem proving.关键词
自动定理证明/二元归结/多元演绎/一阶逻辑/证明器Key words
automated theorem proving/binary resolution/multi-clause deduction/first-order logic/prover分类
计算机与自动化引用本文复制引用
曹锋,杨小玲,易见兵,李俊..基于子句正负文字的多元演绎算法[J].华中科技大学学报（自然科学版）,2025,53(5):157-163,7.基金项目
国家自然科学基金资助项目(62366017,62066018) （62366017,62066018）
江西省教育厅资助项目(GJJ200818,GJJ210828) （GJJ200818,GJJ210828）
赣州市科技计划资助项目(GZKJ20206030) （GZKJ20206030）
江西理工大学博士启动基金资助项目(205200100060). （205200100060）
