计算机应用

作者：刘媛媛, 陈树伟, 宋德培, 杨源骏

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

关键词：一阶逻辑,自动定理证明器,子句动态选择,层次分析法,逼近理想解排序法

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

子句选择是自动定理证明器（ATP）的核心部分，通过优化子句选择方法能够提升ATP的能力和效率。当前，传统基于属性优先级的逐一筛选方法虽然能够实现子句选择，但难以对子句进行全面评估，并且缺乏灵活性。因此，提出基于AHP_TOPSIS的子句动态选择方法。该方法通过层次分析法（AHP）计算子句各个属性的权重，再利用权重结果结合逼近理想解排序法（TOPSIS）对子句进行评估排序，从而为子句选择提供依据。在AHP中，考虑到子句属性的动态变化，引入阶段感知与平滑过渡的方法，使得判断矩阵能够根据推导进程动态调整，将AHP拓展为动态AHP。同时，根据上述子句选择方法实现相应的算法，并将算法应用于一阶逻辑定理证明器CSE（Contradiction Separation Extension）中形成新的证明器CSE_AT。利用该证明器对2021—2024年的TPTP（Thousands of Problems for Theorem Provers）问题库中的一阶逻辑问题进行测试，实验结果表明，CSE_AT比CSE多证明了22个定理，且CSE_AT证明的大部分定理的Rating值集中在［0.6，0.9］。可见，基于AHP_TOPSIS的子句动态选择方法能够优化演绎路径，从而提升证明器的证明能力。

来源：2026年第3期

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

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