计算机应用

作者：姜世攀, 陈树伟, 曾国艳

单位：1.西南交通大学 数学学院，成都 611756；2.系统可信性自动验证国家地方联合工程实验室（西南交通大学），成都 611756

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

基金：国家自然科学基金资助项目(61976130)

在一阶逻辑定理证明器中，子句预处理是不可或缺的步骤，而子句的消去规则是预处理中极其重要的部分。传统的基于纯文字规则的子句消去方法在理论上存在子句删除过多的问题，在算法实现上又存在子句删除不充分的情况。为了提高子句删除的精确率，在理论上，基于纯文字规则对子句进行再分类。第一类称为无效子句，该类子句不能通过等词替换与某个子句形成互补对，此类子句应完全删除；第二类为相对无效子句，该类子句无法与当前子句集中的子句形成互补对，但能进行等词替换，此类子句应在参与演绎后综合考虑是否删除。在算法实现中，考虑到子句的消去应是动态的过程，当前消去的子句会影响已判断的子句的无效性，提出一种用于判定子句无效性的递归遍历算法。将上述子句约简规则应用于证明器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。实验结果表明，所提无效子句约简算法是一种有效的预处理方式，能够提高一阶逻辑子句集的约简精确率，同时能够提高自动定理证明器的证明能力和缩短证明时间。

来源：2024年第3期

《计算机应用》期刊编辑部

查看计算机应用杂志2024年第3期