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

作者：曾国艳; 徐扬^*; 陈树伟; 姜世攀

来源：西南交通大学学报, 2023, 1-8.

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

基于一阶逻辑的自动定理证明器(automatic theorem prover， ATP)作为知识表达和自动推理研究的重要内容，启发式策略是提高ATP性能的研究热点.主流的启发式策略通过描述子句属性，规定属性优先级选择子句，但属性优先级受人为因素影响，评估子句需要花费较长时间. 为此，本文基于矛盾体分离(S-CS)规则，提出新的多属性决策(Multi-Criteria Decision Making， MCDM)子句评估方法.首先，采用熵权法对子句属性客观赋权；其次，结合偏好顺序结构评估法(PROMETHEE II)评估子句，得到子句的完备序；最后，将本文的MCDM方法加入自动定理证明器Contradiction Separation Extension (CSE 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)，并证明了5个Vampire 4.7不能证明的定理，41个E 2.6不能证明的定理，293个Prover9不能证明的定理；在更短的平均时间内，MCDM＿V比Vampire 4.7多证明了6个定理(来自CADE2022)，MCDM＿E比E 2.6多证明了8个定理.

• 单位
  数学学院; 西南交通大学