基于多属性决策的矛盾体分离式评估方法

曹锋; 吴澍康; 朱伟臻; 易见兵

doi:10.16088/j.issn.1001-6600.2025120301

广西师范大学学报（自然科学版） ›› 2026, Vol. 44 ›› Issue (4) : 107 -120. DOI: 10.16088/j.issn.1001-6600.2025120301

基于多属性决策的矛盾体分离式评估方法

曹锋, 吴澍康, 朱伟臻, 易见兵

作者信息 +

Author information +

文章历史 +

摘要

多元演绎方法是基于矛盾体分离规则的自动定理证明器的推理核心，具有不同于二元演绎方法的多元和动态演绎特点。当前，子句选择策略方法是多元演绎研究的热点，能有效优化多元演绎路径，但缺乏针对演绎路径本身进行综合评估。矛盾体分离式评估方法是一种新颖的多元演绎路径评估机制，能较好地指导多元演绎路径搜索。本文将多属性决策方法用于矛盾体分离式评估，首先，对矛盾体分离式进行属性度量，采用熵权法进行客观赋权，并结合多准则优化与折衷解法(VIKOR)评估矛盾体分离式；其次，基于该评估方法提出一种多元演绎算法，在评估矛盾体分离式的同时动态更新其评估标准，能通过回溯机制避免无效路径的搜索，从而有效提升多元演绎的推理能力；最后，将该多元演绎算法应用到国际先进的一阶逻辑自动定理证明器Eprover3.2中，并对2023—2025年国际自动定理证明器竞赛例和TPTP(thousands of problems for theorem provers)库中rating为1的难问题进行测试。结果显示，加入本文算法的Eprover3.2相比原始Eprover3.2分别多证明定理14、14和20个；能证明出9个难度系数为1的定理。实验结果表明，本文提出的多元演绎方法能有效应用于一阶逻辑自动定理证明。