计算机工程与科学2023，Vol.45Issue(12)：2256-2264,9.DOI:10.3969/j.issn.1007-130X.2023.12.017
基于子句活跃度和复杂度的多元动态演绎算法及应用
A multi-clause dynamic deduction algorithm based on clause activity and complexity and its application
摘要
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 deduc-tion 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 dynam-ic 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 Eprov-er 2.6.In addition,it can prove 16 unproven theorems of Eprover 2.6,accounting for 15.1%of the to-tal unproven theorems.The experimental results show that the proposed multi-clause dynamic deduc-tion 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分类
信息技术与安全科学引用本文复制引用
林玲瑜,曹锋,易见兵,方旺盛,李俊,吴贯锋..基于子句活跃度和复杂度的多元动态演绎算法及应用[J].计算机工程与科学,2023,45(12):2256-2264,9.基金项目
国家自然科学基金(62066018,62106206) （62066018,62106206）
江西省科技厅项目(20212ACB202003) （20212ACB202003）
江西省教育厅项目(GJJ200818,GJJ180482) （GJJ200818,GJJ180482）
江西理工大学博士启动基金(205200100060) （205200100060）
