A Multi-clause Dynamic Deduction Algorithm Based on Clause Stability and Its Application
The first-order logic automated theorem proving is the core foundation of artificial intelligence.Heuristic strategies have attracted much attention in improving first-order logic automated theorem provers,and selecting effective clauses based on clause properties to participate in deduction is an important research topic.Based on the standard contradiction separation rule,the literals in clauses are divided into two parts,which are constructing standard contradictory text and constructing contradictory separation text.By analyzing the relationship and differences between variables,functions,and constants,a stability based on clause measurement method is proposed,and its core idea is to evaluate the stability of clause participating in deduction through the components of contained term.A multi-clause dynamic deduction algorithm(CFA,clause stability algorithm)is proposed based on clause stability,aiming to search for optimal paths during the current deduction process.This newly-built CFA algorithm is applied to the internationally well-known prover Prover9 and top prover Eprover2.6,and two new provers CFA_P and CFA_E are formed,respectively.The international competition problems of CASC-26(FOF division)is tested on CFA_P and CFA_E.CFA_P can solve 119 theorems more than the original Prover9,and CFA_E outperforms Eprover2.6,solving 11 theorems more than the original Eprover2.6,and the average proof time of theorems of CFA_P and CFA_E is reduced by 14.76 s and 2.54 s,respectively with the same total number of solved theorems.Focusing on the 94 theorems unsolved by Eprover2.6,CFA_E solves 27 theorems which accounts for 28.7％in the total.The experimental results demonstrate the effectiveness of the CFA algorithm,which has good performance in optimizing deduction paths and can enhance the performance of first-order logic automated theorem prover.
万方数据
维普
