基于目标演绎距离的一阶逻辑子句集预处理方法

First-order Logic Clause Set Preprocessing Method Based on Goal Deduction Distance

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

The first-order logic theorem proving is the core foundation of artificial intelligence,it has great academic significance to study the theory and efficient algorithm implementation for first-order logic automated theorem provers.The current provers adopt clause set preprocessing approaches to reduce clause set scale,then apply inference rules to prove theorems.The existing clause set preprocessing method used in provers is generally only from the perspective of the semantic relevance to axioms and conjecture,and it can't reflect the deduction between clauses well from the complementary pairs of literals point of view.In order to describe the relationship between clauses from the perspective of deduction,the definition of goal deduction distance and the calculation method are proposed,and a first-order logic clause set preprocessing method is presented based on the proposed goal deduction distance.Firstly,the original clause set is applied with redundant clause simplification and pure literal deletion rule.Then,taking the goal clauses into consideration,the literal goal deduction distance and the clause goal deduction distance are calculated,and finally further clause set preprocessing is realized by the setting threshold of clause deduction distance.We implement the proposed clause set preprocessing method in Vampire that is the winner of the 2017 CADE ATP System Competition(CASC-26)FOF division,and apply it to solve the CASC-26 problem.Within the standard 300 seconds,the top prover Vampire4.1 with the proposed clause set preprocessing method outperforms Vampire4.1 by solving 4 theorems more than Vampire4.1,and 10 out of the 74 problems unsolved by Vampire4.1,accounting for 13.5%of the total.The proposed clause set preprocessing method has affected 77.2%of the solved theorems,and the largest reduction proportion is 51.7%.Experimental results show that the proposed first-order logic clause set preprocessing method is an effective method,which can effectively reduce the clause set scale and improve the ability of first-order logic automated theorem prover.