关键词: 一阶逻辑, 定理证明, 自动推理, 多元动态演绎, 子句评估

Abstract: First-order logic automated theorem proving is an important research content in the fields of knowledge representation and automated reasoning. How to effectively select clauses to participate in deduction is a research hotspot to improve the capability and efficiency of automated reasoning. Based on the good de-duction characteristics of multi-clause dynamic deduction, this paper proposes a measure and calculation method of clause activity and complexity by analyzing the properties of the variable terms and the structure of function terms of clauses, which can effectively evaluate clauses with different term structures. Based on the clause evaluation method, a multi-clause dynamic deduction algorithm with fully synergized deduction of clauses is proposed, which can effectively optimize the multi-clause deduction search path. The multi-clause dynamic deduction algorithm is applied to the international top prover Eprover 2.6, and the 2021 international automated reasoning competition problems (FOF group) is used as the test object. Within the standard 300 seconds, Eprover 2.6 with the proposed multi-clause dynamic deduction algorithm proven four more theorems than the original Eprover 2.6, and the average proof time is decreases by 1.12 seconds under the condition of proving the same number of theorems as Eprover 2.6. In addition, it can prove 16 unproven theorems of Eprover 2.6, accounting for 15.1% of the total unproven theorems. The experimental results show that the proposed multi-clause dynamic deduction algorithm is an effective inference method, which can improve the capability and time efficiency of automated reasoning to a certain extent. 

Key words: first-order logic, theorem proving, automated reasoning, multi-clause dynamic deduction, clause evaluation