一种基于子句充分性评估的多元动态演绎算法及应用

作     者：曹锋 潘世成 易见兵 李俊 

作者机构：江西理工大学信息工程学院 

出 版 物：《华中科技大学学报(自然科学版)》 (Journal of Huazhong University of Science and Technology(Natural Science Edition))

年 卷 期：2023年

核心收录：

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 081104[工学-模式识别与智能系统] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金项目(62066018、62106206) 

主　　题：多元动态演绎 回溯机制 一阶逻辑 二元链式演绎 自动定理证明器 

摘      要：与二元链式演绎方法相比，多元动态演绎生成的新子句常含有较少的文字数。通过分析多元动态演绎的演绎过程表明，子句的充分性演绎能进一步提升多元演绎的效率。为了充分体现子句参与多元动态演绎的灵活性、协同性和充分性，本文将参与多元演绎的子句划分为主动子句和被动子句，提出了一种不同类型的子句充分性评估方法，能较好地体现子句的充分性演绎并避免重复路径的搜索；基于该子句评估方法提出了一种充分使用子句的多元动态演绎算法，能通过回溯机制搜索较优的演绎路径。将该算法应用于国际顶尖的证明器Eprover中，以2020年和2021年国际一阶逻辑自动定理证明器竞赛例（FOF组）为测试对象，在标准测试时间300秒内，加入了本文多元动态演绎算法的Eprover2.4分别比原始Eprover2.4多证明定理11个和9个，能证明Eprover2.4无法证明的定理分别为14个和13个；以TPTP问题库中rating为1的定理作为测试对象，加入了本文多元动态演绎算法的Eprover2.4能有效证明出7个所有证明器都未证明的定理。实验结果表明，加入提出的多元动态演绎算法的证明器Eprover定理证明能力得到了有效的提升，本文提出的多元动态演绎算法能有效应用于一阶逻辑自动定理证明。