文件名称：基于目标演绎距离的一阶逻辑子句集预处理方法_曹锋.pdf
文件大小：539KB
文件格式：PDF
更新时间：2022-12-10 12:31:31
一阶逻辑; 人工智能; 子句集预处理; 演绎距离; 冗余子句;
一阶逻辑定理证明是人工智能的核心基础，研究一阶逻辑自动定理证明器相关理论和高效的算法实现具有重要的学术意义。当前一阶逻辑自动定理证明器首先通过子句集预处理约简子句集规模，然后通过演绎方法对定理进行判定。现有的应用于证明器中的子句集预处理方法普遍只从与目标子句项符号相关性角度出发，不能很好地从文字的互补对关系中体现子句间的演绎。为了在子句集预处理时从演绎的角度刻画子句间的关系，定义了目标演绎距离的概念并给出了计算方法，提出了一种基于目标演绎距离的一阶逻辑子句集预处理方法。首先对原始子句集进行包含冗余子句约简和应用纯文字删除规则，然后根据目标子句计算剩余子句集中的文字目标演绎距离、子句目标演绎距离，并最终通过设定子句演绎距离阈值来实现对子句集的进一步预处理。将该预处理方法应用于顶尖证明器Vampire，以2017年国际一阶逻辑自动定理证明器标准一阶逻辑问题组竞赛例为测试对象，在标准的300 s内，加入提出的子句集预处理方法的Vampire4.1相比原始的Vampire4.1多证明定理4个，能证明10个Vampire4.1未证明的定理，占其未证明定理总数的13.5%，在证明的定理中，提出的子