A Multi-Clause Conflict Deduction Method Based on Contradiction Separation and Its Application
The conflict deduction method based on binary resolution handles only two clauses in each deduction step,and its efficiency in seeking conflict deduction needs improvement.We propose a multi-clause conflict deduction method based on contradiction separation,and the definition of contradiction separation multi-clause conflict deduction,methods of generation learning clauses,the proof of deduction soundness,its deduction characteristics,advantages analysis of the deduction method,and the selection method of weak clause are given.In the deduction process of seeking conflict,the proposed conflict deduction method allows multiple(two or more)clauses to be involved in each deduction step,which makes it easier to generate conflicts and handle clauses with many literals,thus improving the efficiency of conflict deduction.The experimental results show that the contradiction separation multi-clause conflict deduction method has better reasoning capability,and solves more theorems with the less average proof time than the binary conflict deduction method.The Eprover equipped with our contradiction separation multi-clause conflict deduction method shows high efficiency in search and proof task,making it well-suited for automated theorem proving in first-order logic,particularly for complex problems.
万方数据
