基于AHP_TOPSIS的子句动态选择方法

doi:10.11772/j.issn.1001-9081.2025030382

《计算机应用》唯一官方网站 ›› 2026, Vol. 46 ›› Issue (3): 715-722.DOI: 10.11772/j.issn.1001-9081.2025030382

基于AHP_TOPSIS的子句动态选择方法

刘媛媛¹^,², 陈树伟¹^,²(), 宋德培¹, 杨源骏¹

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

收稿日期:2025-04-14 修回日期:2025-07-01 接受日期:2025-07-03 发布日期:2026-03-16 出版日期:2026-03-10
通讯作者: 陈树伟
作者简介:刘媛媛（2001—），女，四川巴中人，硕士研究生，主要研究方向：自动推理
宋德培（2002—），男，四川成都人，硕士研究生，主要研究方向：自动推理
杨源骏（2002—），男，四川眉山人，硕士研究生，主要研究方向：自动推理。
基金资助:
国家自然科学基金资助项目(12301595)

Dynamic clause selection method based on AHP_TOPSIS

Yuanyuan LIU¹^,², Shuwei CHEN¹^,²(), Depei SONG¹, Yuanjun YANG¹

^1.School of Mathematics，Southwest Jiaotong University，Chengdu Sichuan 611756，China
^2.National-Local Joint Engineering Laboratory of System Credibility Automatic Verification （Southwest Jiaotong University），Chengdu Sichuan 611756，China

Received:2025-04-14 Revised:2025-07-01 Accepted:2025-07-03 Online:2026-03-16 Published:2026-03-10
Contact: Shuwei CHEN
About author:LIU Yuanyuan， born in 2001， M. S. candidate. Her research interests include automated reasoning.
SONG Depei， born in 2002， M. S. candidate. His research interests include automated reasoning.
YANG Yuanjun， born in 2002， M. S. candidate. His research interests include automated reasoning.
Supported by:
National Natural Science Foundation of China(12301595)

摘要/Abstract

摘要：

子句选择是自动定理证明器（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的子句动态选择方法能够优化演绎路径，从而提升证明器的证明能力。

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

Abstract:

Clause selection is the core part of Automated Theorem Prover （ATP）， the ability and efficiency of ATP can be improved by optimizing the clause selection method. At present， although the traditional one-by-one filtering method based on attribute priority can realize clause selection， it is difficult to evaluate clause comprehensively and lacks flexibility. Therefore， a dynamic clause selection method based on AHP_TOPSIS was proposed. In the method， the weight of each attribute of the clause was calculated by Analytic Hierarchy Process （AHP）， and then the clauses were evaluated and ranked by combining the weight results with Technique for Order Preference by Similarity to an Ideal Solution （TOPSIS）， thereby providing a basis for clause selection. In the AHP， considering the dynamic change of clause attributes， the methods of stage awareness and smooth transition were introduced. This enables the judgment matrix to be adjusted dynamically according to the derivation process， thus extending the AHP to the dynamic AHP. Meanwhile， according to the above clause selection method， the corresponding algorithm was implemented and applied to the first-order logic theorem prover CSE （Contradiction Separation Extension） to form a new prover CSE_AT. This prover was used to test the first-order logic problems in the TPTP （Thousands of Problems for Theorem Provers） problem bank from 2021 to 2024. Experimental results show that CSE_AT proves 22 more theorems than CSE， and most of the theorems proved by CSE_AT have Rating value in the range of ［0.6，0.9］. It can be seen that the AHP_TOPSIS-based dynamic clause selection method can optimize the deductive paths， so as to improve the proof ability of the prover.

Key words: first-order logic, Automated Theorem Prover (ATP), dynamic clause selection, Analytic Hierarchy Process (AHP), Technique for Order Preference by Similarity to an Ideal Solution (TOPSIS)

中图分类号:

TP181

刘媛媛, 陈树伟, 宋德培, 杨源骏. 基于AHP_TOPSIS的子句动态选择方法[J]. 计算机应用, 2026, 46(3): 715-722.

Yuanyuan LIU, Shuwei CHEN, Depei SONG, Yuanjun YANG. Dynamic clause selection method based on AHP_TOPSIS[J]. Journal of Computer Applications, 2026, 46(3): 715-722.

图/表 5

表1 矛盾体分离的演绎过程

Tab. 1 Deductive process of contradiction separation

$C i$	$σ i$	$C i σ i -$	$C i σ i +$
$C 1$		$P 1 a ∨ ¬ P 2 b$
$C 2$	$c / x 1$	$P 3 c ∨ P 4 c$	$¬ P 2 f a$
$C 3$	$a / x 2$	$¬ P 1 a$
$C 4$	$b / x 3, c / x 4$	$P 2 b ∨ ¬ P 3 c$
$C 5$		$P 1 a ∨ ¬ P 4 c$

表1 矛盾体分离的演绎过程

Tab. 1 Deductive process of contradiction separation

$C i$	$σ i$	$C i σ i -$	$C i σ i +$
$C 1$		$P 1 a ∨ ¬ P 2 b$
$C 2$	$c / x 1$	$P 3 c ∨ P 4 c$	$¬ P 2 f a$
$C 3$	$a / x 2$	$¬ P 1 a$
$C 4$	$b / x 3, c / x 4$	$P 2 b ∨ ¬ P 3 c$
$C 5$		$P 1 a ∨ ¬ P 4 c$

图1 本文方法的流程

Fig. 1 Flow of proposed method

图2 CSE_AT的流程

Fig. 2 Flow of CSE_AT

表2 CSE_AT与CSE的证明情况对比

Tab. 2 Comparison of proof conditions between CSE_AT and CSE

问题库年份	共同证明定理数	CSE单独证明定理数	CSE_AT单独证明定理数
总数	379	136	158
2021	108	40	48
2022	106	31	34
2023	83	31	36
2024	82	34	40

图3 CSE_AT与CSE证明定理难度等级对比

Fig. 3 Comparison of difficulty level between CSE_AT and CSE in proving theorems

参考文献 24

[1]	CHATTERJEE P， ROY S， DIEP B P， et al. Distributed bounded model checking ［J］. Formal Methods in System Design， 2024， 64（1）： 50-72.
[2]	McCUNE W. Solution of the Robbins problem ［J］. Journal of Automated Reasoning， 1997， 19（3）： 263-276.
[3]	KOVÁCS L. Symbolic computation and automated reasoning for program analysis ［C］// Proceedings of the 2016 International Conference on Integrated Formal Methods， LNCS 9681. Cham： Springer， 2016： 20-27.
[4]	SCHULZ S， CRUANES S， VUKMIROVIĆ P. Faster， higher， stronger： E 2.3 ［C］// Proceedings of the 2019 International Conference on Automated Deduction， LNCS 11716. Cham： Springer， 2019： 495-507.
[5]	KOVÁCS L， VORONKOV A. First-order theorem proving and Vampire ［C］// Proceedings of the 2013 International Conference on Computer Aided Verification， LNCS 8044. Berlin： Springer， 2013： 1-35.
[6]	XU Y， LIU J， CHEN S， et al. Contradiction separation based dynamic multi-clause synergized automated deduction ［J］. Information Sciences， 2018， 462： 93-113.
[7]	曹锋. 一种基于矛盾体分离演绎的一阶逻辑自动定理证明器研究［D］. 成都：西南交通大学， 2020： 58-93.
	CAO F. Study on a first-order logic automated theorem prover based on contradiction separation and deduction ［D］. Chengdu： Southwest Jiaotong University， 2020： 58-93.
[8]	SCHULZ S， MÖHRMANN M. Performance of clause selection heuristics for saturation-based theorem proving ［C］// Proceedings of the 2016 International Joint Conference on Automated Reasoning， LNCS 9706. Cham： Springer， 2016： 330-345.
[9]	RAWSON M， REGER G. Old or heavy？ decaying gracefully with age/weight shapes ［C］// Proceedings of the 2019 International Conference on Automated Deduction， LNCS 11716. Cham： Springer， 2019： 462-476.
[10]	TAMMET T. GKC： a reasoning system for large knowledge bases［C］// Proceedings of the 2019 International Conference on Automated Deduction， LNCS 11716. Cham： Springer， 2019： 538-549.
[11]	ABDELAZIZ I， CROUSE M， MAKNI B， et al. Learning to guide a saturation-based theorem prover ［J］. IEEE Transactions on Pattern Analysis and Machine Intelligence， 2023， 45（1）： 738-751.
[12]	HOLDEN E K， KOROVIN K. Heterogeneous heuristic optimisation and scheduling for first-order theorem proving ［C］// Proceedings of the 2021 International Conference on Intelligent Computer Mathematics， LNCS 12833. Cham： Springer， 2021： 107-123.
[13]	ZHONG J， XU Y， CAO F. A novel combinational ATP based on contradiction separation for first order logic ［J］. International Journal of Computational Intelligence Systems， 2020， 13（1）： 672-680.
[14]	LIU P， XU Y， LIU J， et al. Fully reusing clause deduction algorithm based on standard contradiction separation rule ［J］. Information Sciences， 2023， 622： 337-356.
[15]	林玲瑜，曹锋，易见兵，等. 基于子句活跃度和复杂度的多元动态演绎算法及应用［J］. 计算机工程与科学， 2023， 45（12）： 2256-2264.
	LIN L Y， CAO F， YI J B， et al. A multi-clause dynamic deduction algorithm based on clause activity and complexity and its application ［J］. Computer Engineering and Science， 2023， 45（12）： 2256-2264.
[16]	曾国艳，徐扬，陈树伟，等. 基于多属性决策的一阶逻辑子句选择方法［J］. 西南交通大学学报， 2025， 60（1）： 185-193.
	ZENG G Y， XU Y， CHEN S W， et al. First-order logic clause selection method based on multi-criteria decision making ［J］. Journal of Southwest Jiaotong University， 2025， 60（1）： 185-193.
[17]	姜世攀，陈树伟，曾国艳. 一阶逻辑定理证明器中的无效子句删除策略［J］. 计算机应用， 2024， 44（3）： 677-682.
	JIANG S P， CHEN S W， ZENG G Y. Strategy of invalid clause elimination in first-order logic theorem prover ［J］. Journal of Computer Applications， 2024， 44（3）： 677-682.
[18]	SAATY T L， VARGAS L G. The seven pillars of the analytic hierarchy process ［M］// Models， methods， concepts & applications of the analytic hierarchy process， ISOR 175. ed2nd. New York： Springer， 2012： 23-40.
[19]	HWANG C L， YOON K. Methods for multiple attribute decision making ［M］// Multiple attribute decision making： methods and applications a state-of-the-art survey， LNE 186. Berlin： Springer， 1981： 58-191.
[20]	GLEISS B， SUDA M. Layered clause selection for saturation-based theorem proving ［C］// Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop. Aachen： CEUR-WS.org， 2020： 34-52.
[21]	李庆扬，王能超，易大义. 数值分析［M］. 5版. 北京：清华大学出版社， 2008： 22-29.
	LI Q Y， WANG N C， YI D Y. Numerical analysis ［M］. 5th ed. Beijing： Tsinghua University Press， 2008： 22-29.
[22]	SUTCLIFFE G. The CADE ATP system competition — CASC ［J］. AI Magazine， 2016， 37（2）： 99-101.
[23]	The CADE ATP system competition： the world championship for automated theorem proving ［EB/OL］. ［2025-03-24］..
[24]	SUTCLIFFE G. The TPTP problem library and associated infrastructure ［J］. Journal of Automated Reasoning， 2017， 59（4）： 483-502.

基于AHP_TOPSIS的子句动态选择方法

Dynamic clause selection method based on AHP_TOPSIS

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 5

参考文献 24

相关文章 15

编辑推荐

Metrics

[1]	余鹰, 朱锋, 付红剑, 罗逸文, 钱进, 郑宇超. 联合三支决策与熵权TOPSIS的专家反评估模型[J]. 《计算机应用》唯一官方网站, 2025, 45(5): 1424-1431.
[2]	姚洪磊, 刘吉强, 童恩栋, 牛温佳. 基于 α-截集三角模糊数和攻击树的CTCS网络安全风险评估方法[J]. 《计算机应用》唯一官方网站, 2024, 44(4): 1018-1026.
[3]	姜世攀, 陈树伟, 曾国艳. 一阶逻辑定理证明器中的无效子句删除策略[J]. 《计算机应用》唯一官方网站, 2024, 44(3): 677-682.
[4]	孙延浩, 许伟, 张涛, 刘宁馨. 考虑决策者心理行为的软件质量评价方法[J]. 《计算机应用》唯一官方网站, 2022, 42(8): 2528-2533.
[5]	李炜, 吴群群, 张以文. 基于E-CARGO模型的开发者推荐方法[J]. 《计算机应用》唯一官方网站, 2022, 42(2): 557-564.
[6]	李付民, 佟玲玲, 杜翠兰, 李扬曦, 张仰森. 基于关联关系的微博用户可信度分析方法[J]. 计算机应用, 2017, 37(3): 654-659.
[7]	刘莹, 张涛, 李坤, 李楠. 移动应用众包测试人员评价模型[J]. 计算机应用, 2017, 37(12): 3569-3573.
[8]	杜元伟, 石方园, 杨娜. 基于证据理论/层次分析法的贝叶斯网络建模方法[J]. 计算机应用, 2015, 35(1): 140-146.
[9]	杨超燕雪峰张洁周勇. 基于权重的云推理算法[J]. 计算机应用, 2014, 34(2): 501-505.
[10]	江正华. 基于方差的最优组合赋权模型在网络信息资源评价中的应用[J]. 计算机应用, 2014, 34(1): 302-308.
[11]	赵华琼唐学文. 基于模糊层次分析法的网络业务性能评估模型[J]. 计算机应用, 2013, 33(11): 3035-3038.
[12]	王威付晓东夏永滢田强李昌志. Web服务组合评分分配方法[J]. 计算机应用, 2013, 33(11): 3252-3256.
[13]	罗彪闫维维万亮. 基于ANP和K-means聚类的客户价值分类模型及应用[J]. 计算机应用, 2013, 33(10): 2954-2959.
[14]	卢志刚朱文瑾. 基于修正区间模糊Shapley值信息产品供应链利益分配算法[J]. 计算机应用, 2013, 33(10): 2960-2963.
[15]	李跃宗王鹏玲林轩王青元. 高速列车自动驾驶优化算法[J]. 计算机应用, 2012, 32(11): 3221-3224.