基于多属性决策的一阶逻辑子句选择方法

作     者：曾国艳 徐扬 陈树伟 姜世攀 ZENG Guoyan;XU Yang;CHEN Shuwei;JIANG Shipan

作者机构：西南交通大学数学学院四川成都611756 西南交通大学系统可信性自动验证国家地方联合工程实验室四川成都611756 

出 版 物：《西南交通大学学报》 (Journal of Southwest Jiaotong University)

年 卷 期：2025年第60卷第1期

页      面：185-193页

核心收录：

学科分类：07[理学] 08[工学] 0835[工学-软件工程] 0701[理学-数学] 081202[工学-计算机软件与理论] 070101[理学-基础数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

主　　题：一阶逻辑 矛盾体分离规则 启发式策略 多属性决策 熵权法 

摘      要：基于一阶逻辑的自动定理证明器(ATP)在知识表达和自动推理研究中占据重要地位,而启发式策略则是提升ATP性能的关键研究方向.主流的启发式策略通常通过描述子句属性来确定属性优先级,从而选择子句,但属性优先级受人为因素影响,且评估子句耗时较长.为此,本文基于矛盾体分离(S-CS)规则,提出一种新的多属性决策(MCDM)子句评估方法.首先,利用熵权法对子句属性进行客观赋权;其次,结合偏好顺序结构评估法(PROMETHEEⅡ)对子句进行评估,得到子句的完全排序;最后,将提出的MCDM方法加入自动定理证明器CSE 1.5(contradiction separation extension 1.5)、Vampire 4.7和Eprover(E 2.6)中,分别形成新的证明器MCDM_CSE、MCDM_V和MCDM_E.对MCDM_CSE测试了国际定理证明器问题库TPTP(Thousands of Problems for Theorem Provers)中一阶逻辑格式的定理,并对MCDM_V和MCDM_E测试了2022年CADE(Conference on Automated Deduction)竞赛例(一阶逻辑组).实验表明:MCDM_CSE比CSE 1.5多证明了151个定理(来自TPTP),并且能够证明Vampire 4.7无法证明的5个定理、E 2.6无法证明的41个定理以及Prover9无法证明的293个定理;在更短的平均时间内,MCDM_V比Vampire 4.7多证明了6个定理(来自CADE 2022),MCDM_E比E 2.6多证明了8个定理.