Abstract:

In the first-order logic theorem prover， clause preprocessing is an essential step， and the rule of clause elimination is an extremely important part of preprocessing. The traditional clause elimination method based on pure literal rules has some drawbacks which more than enough clauses should be deleted in theory， while less clauses were deleted during implementation. In order to make the clause elimination more accurate， the clauses were classified based on pure literal rules. The first category was called the invalid clause which was not able to form complementary pair to any clause in the clause set through equivalence substitution， and should be completely deleted. The second category was called the relatively invalid clause， which was not complementary to any clause in the current clause set， but could be replaced by other clause after equivalence substitution and should be deleted after certain deduction steps. The clause elimination should actually be a dynamic process where the current clause elimination would affect the invalidity of the determined clauses. Therefore， a clause elimination recursive traversal algorithm for determining clause invalidity was presented and implemented to the prover CSE1.5 （Contradiction Separation Extension 1.5）. The problems in first-order logic problem group of the CADE （Conference on Automated DEduction） Automated Theorem Proving （ATP） system competition from 2019 to 2022 were used as the test problems. The CSE1.5_IC with the invalid clause elimination algorithm proved 27 more problems than original CSE1.5 in 300 s. Among all the FNE （FOF theorems without Equality） test cases jointly proved by the two versions of the prover， CSE1.5_IC eliminated 28 more invalid clauses per problem on average than CSE1.5， and the average solution time was reduced by 7.07 s. The experimental results show that the proposed invalid clause elimination algorithm is an effective preprocessing method， which increases the reduction accuracy in the first-order logical clause set， and improves the proving ability and shortens the proof time of automatic theorem prover.

Key words: automatic reasoning, first-order logic, clause elimination, pure literal rule, invalid clause

摘要：

在一阶逻辑定理证明器中，子句预处理是不可或缺的步骤，而子句的消去规则是预处理中极其重要的部分。传统的基于纯文字规则的子句消去方法在理论上存在子句删除过多的问题，在算法实现上又存在子句删除不充分的情况。为了提高子句删除的精确率，在理论上，基于纯文字规则对子句进行再分类。第一类称为无效子句，该类子句不能通过等词替换与某个子句形成互补对，此类子句应完全删除；第二类为相对无效子句，该类子句无法与当前子句集中的子句形成互补对，但能进行等词替换，此类子句应在参与演绎后综合考虑是否删除。在算法实现中，考虑到子句的消去应是动态的过程，当前消去的子句会影响已判断的子句的无效性，提出一种用于判定子句无效性的递归遍历算法。将上述子句约简规则应用于证明器CSE1.5（Contradiction Separation Extension 1.5）中，以2019—2022的CADE（Conference on Automated DEduction）自动定理证明（ATP）系统竞赛中一阶逻辑问题组为测试对象。在300 s内，应用所提算法的CSE1.5_IC比原始CSE1.5总共多证明了27个问题。在两个版本证明器共同证明的所有FNE（FOF theorems without Equality）测试例中，CSE1.5_IC比CSE1.5平均每个问题多约简了28个子句，平均求解时间减少了7.07 s。实验结果表明，所提无效子句约简算法是一种有效的预处理方式，能够提高一阶逻辑子句集的约简精确率，同时能够提高自动定理证明器的证明能力和缩短证明时间。

关键词: 自动推理, 一阶逻辑, 子句删除, 纯文字规则, 无效子句