子句选择是自动定理证明器(ATP)的核心部分,通过优化子句选择方法能够提升ATP的能力和效率。当前,传统基于属性优先级的逐一筛选方法虽然能够实现子句选择,但难以对子句进行全面评估,并且缺乏灵活性。因此,提出基于AHP_TOPSIS的子句动...子句选择是自动定理证明器(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的子句动态选择方法能够优化演绎路径,从而提升证明器的证明能力。展开更多
文摘子句选择是自动定理证明器(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的子句动态选择方法能够优化演绎路径,从而提升证明器的证明能力。
