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

• 智能信息处理 • 上一篇    下一篇

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

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

  1. 1.江西理工大学 信息工程学院, 江西 赣州 341000;
    2.多维智能感知与控制江西省重点实验室(江西理工大学), 江西 赣州 341000
  • 收稿日期:2025-12-03 修回日期:2026-02-28 出版日期:2026-07-05 发布日期:2026-07-01
  • 通讯作者: 曹锋(1984—), 男, 江西上饶人, 江西理工大学副教授, 博士。E-mail: caofeng19840301@163.com
  • 基金资助:
    国家自然科学基金(62366017,62066018);江西省教育厅项目(GJJ200818,GJJ210828);江西理工大学博士启动基金(205200100060)

Evaluation of contradiction separation clause based on multi-criteria decision making

Cao Feng1,2*, Wu Shukang1,2, Zhu Weizhen1,2, Yi Jianbing1,2   

  1. 1. School of Information Engineering, Jiangxi University of Science and Technology, Ganzhou Jiangxi 341000, China;
    2. Jiangxi Province Key Laboratory of Multidimensional Intelligent Perception and Control (Jiangxi University of Science and Technology), Ganzhou Jiangxi 341000, China
  • Received:2025-12-03 Revised:2026-02-28 Online:2026-07-05 Published:2026-07-01

PDF (PC)

1

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

关键词: 多元演绎, 矛盾体分离规则, 定理证明器, 子句选择策略, 一阶逻辑

Abstract: The multi-clause deduction algorithm is the reasoning core of automated theorem provers based on the contradiction separation rule. It is characterized by multi-clause and dynamic deduction features that differ from binary deduction methods. Currently, clause selection strategy methods are a hotspot in research on multi-clause deduction, effectively optimizing multi-clause deduction paths. However, there is a lack of comprehensive evaluation aimed specifically at the deduction paths themselves. The standard contradiction separation clause evaluation method is a novel multi-clause deduction path evaluation mechanism that can effectively guide the search for multi-clause deduction paths. The multi-criteria decision making method is applied to the evaluation of standard contradiction separation clause. Firstly, the attribute of the contradiction separation clause is measured, objectively weighted using the entropy weight method, and evaluated through a combination of multi-criteria optimization and compromise solutions. Secondly, based on this evaluation method, a multi-clause deduction algorithm is proposed, which can evaluate the standard. Finally, this multi-clause deduction algorithm is applied to the international advanced first-order logic contradiction separation clause while dynamically updating its evaluation criteria. It can avoid searching for invalid paths through a backtracking mechanism, thereby effectively improving the inference ability of multi-clause deduction. The proposed algorithm is implemented in the automated theorem prover Eprover 3.2 and tested on the problems from the last three years of international automated theorem provers competition and TPTP (Thousands of Problems for Theorem Provers) problem library with a rating of 1. Eprover3.2 with the proposed algorithm solves 14, 14 and 20 additional theorems compared with the original Eprover3.2 respectively, and it also solves 9 theorems with a rating of 1. The experimental results show that the proposed multi-clause deduction method can be effectively applied to the first-order logic automated theorem proving.

Key words: multi-clause deduction, contradiction separation rule, theorem prover, clause selection strategies, first-order logic

中图分类号:  TP181

[1] Kovács L. Symbolic computation and automated reasoning for program analysis[C]//Integrated Formal Methods: LNCS Volume 9681. Cham: Springer International Publishing AG Switzerland, 2016: 20-27. DOI: 10.1007/978-3-319-33693-0_2.
[2] O’Hearn P W. Incorrectness logic[J]. Proceedings of the ACM on Programming Languages, 2020, 4: 1-32. DOI: 10.1145/3371078.
[3] Reger G, Voronkov A. Induction in saturation-based proof search[C]//Automated Deduction-CADE 27. Cham: Springer Nature Switzerland AG, 2019: 477-494. DOI: 10.1007/978-3-030-29436-6_28.
[4] Bellomarini L, Benedetto D, Gottlob G, et al. Vadalog: a modern architecture for automated reasoning with large knowledge graphs[J]. Information Systems, 2022, 105: 101528. DOI: 10.1016/j.is.2020.101528.
[5] Quaresma P. Automatic deduction in an AI geometry book[C]//Artificial Intelligence and Symbolic Computation. Cham: Springer Nature Switzerland AG, 2018: 221-226. DOI: 10.1007/978-3-319-99957-9_16.
[6] Pavlov V, Schukin A, Cherkasova T. Exploring automated reasoning in first-order logic: tools, techniques and application areas[J]. Knowledge Engineering and the Semantic Web. Berlin: Springer-Verlag, 2013: 102-116. DOI: 10.1007/978-3-642-41360-5_9.
[7] Robinson J A. A machine-oriented logic based on the resolution principle[J]. Journal of the ACM, 1965, 12(1): 23-41. DOI: 10.1145/321250.321253.
[8] Xu Y, Liu J, Chen S W, et al. Contradiction separation based dynamic multi-clause synergized automated deduction[J]. Information Sciences, 2018, 462: 93-113. DOI: 10.1016/j.ins.2018.04.086.
[9] Cao F, Xu Y, Liu J, et al. A multi-clause dynamic deduction algorithm based on standard contradiction separation rule[J]. Information Sciences, 2021, 566: 281-299. DOI: 10.1016/j.ins.2021.03.015.
[10] 曹锋, 郭海林, 易见兵, 等. 基于矛盾体分离的多元冲突演绎方法及应用[J]. 武汉大学学报(理学版), 2024, 70(6): 671-679. DOI: 10.14188/j.1671-8836.2023.0181.
[11] 林玲瑜, 曹锋, 易见兵, 等. 基于子句活跃度和复杂度的多元动态演绎算法及应用[J]. 计算机工程与科学, 2023, 45(12): 2256-2264. DOI: 10.3969/j.issn.1007-130X.2023.12.017.
[12] Zeng G Y, Chen S W, Liu J, et al. A complementary ratio based clause selection method for contradiction separation dynamic deduction[J]. Knowledge-Based Systems, 2024, 284: 111238. DOI: 10.1016/j.knosys.2023.111238.
[13] 曹锋, 杨小玲, 易见兵, 等. 基于子句正负文字的多元演绎算法[J]. 华中科技大学学报(自然科学版), 2025, 53(5): 157-163. DOI: 10.13245/j.hust.250191.
[14] Liu P Y, Xu Y, Liu J, et al. Fully reusing clause deduction algorithm based on standard contradiction separation rule[J]. Information Sciences, 2023, 622: 337-356. DOI: 10.1016/j.ins.2022.11.128.
[15] 刘媛媛, 陈树伟, 宋德培, 等. 基于AHP_TOPSIS的子句动态选择方法[J]. 计算机应用, 2026, 46(3): 715-722.DOI: 10.11772/j.issn.1001-9081.2025030382.
[16] Schon C. Using the meaning of symbol names to guide first-order logic reasoning[C]//10th Workshop on Formal and Cognitive Reasoning. Aachen: CEUR-WS, 2024: 19-27.
[17] 曾国艳, 徐扬, 陈树伟, 等. 基于多属性决策的一阶逻辑子句选择方法[J]. 西南交通大学学报, 2025, 60(1): 185-193. DOI: 10.3969/j.issn.0258-2724.20230023.
[18] Vukmirović P, Blanchette J, Schulz S. Extending a high-performance prover to higher-order logic[C]//Tools and Algorithms for the Construction and Analysis of Systems: LNCS Volume 13994. Cham: Springer Nature Switzerland AG, 2023: 111-129. DOI: 10.1007/978-3-031-30820-8_10.
[19] 王国俊. 数理逻辑引论与归结原理[M]. 2版. 北京: 科学出版社, 2006: 17-18.
[20] Cao F, Xu Y, Chen S W, et al. A contradiction separation dynamic deduction algorithm based on optimized proof search[J]. International Journal of Computational Intelligence Systems, 2019, 12(2): 1245-1254. DOI: 10.2991/ijcis.d.191022.002.
[21] 曹锋. 一种基于矛盾体分离演绎的一阶逻辑自动定理证明器研究[D]. 成都: 西南交通大学, 2020: 50-51.
[22] 曹锋, 徐扬, 钟建, 等. 基于目标演绎距离的一阶逻辑子句集预处理方法[J]. 计算机科学, 2020, 47(3): 217-221. DOI: 10.11896/jsjkx.190100004.
[23] Zhu Y X, Tian D Z, Yan F. Effectiveness of entropy weight method in decision-making[J]. Mathematical Problems in Engineering, 2020, 2020(1): 3564835. DOI: 10.1155/2020/3564835.
[24] Jiang L L, Wang H, Tong A H, et al. The measurement of green finance development index and its poverty reduction effect: dynamic panel analysis based on improved entropy method[J]. Discrete Dynamics in Nature and Society, 2020, 2020(1): 8851684. DOI: 10.1155/2020/8851684.
[25] Hwang C L, Yoon K. Methods for multiple attribute decision making[M]//Multiple Attribute Decision Making. Berlin: Springer-Verlag, 1981: 58-191. DOI: 10.1007/978-3-642-48318-9_3.
[26] Brans J P, Vincke P. A preference ranking organisation method: the PROMETHEE method for multiple criteria decision-making[J]. Management Science, 1985, 31(6): 647-656. DOI: 10.1287/mnsc.31.6.647.
[27] Park J H, Cho H J, Kwun Y C. Extension of the VIKOR method for group decision making with interval-valued intuitionistic fuzzy information[J]. Fuzzy Optimization and Decision Making, 2011, 10(3): 233-253. DOI: 10.1007/s10700-011-9102-9.
[28] 张帅, 张继飞. 基于两种MCDM的四川汶川县农村环境保护和社会经济综合发展评估[J]. 农业工程学报, 2023, 39(15): 228-238. DOI: 10.11975/j.issn.1002-6819.202304100.
[29] Sutcliffe G. The TPTP problem library and associated infrastructure[J]. Journal of Automated Reasoning, 2017, 59(4): 483-502. DOI: 10.1007/s10817-017-9407-7.
[30] 曹锋, 王家帆, 易见兵, 等. 一种基于子句稳定度的多元动态演绎算法及应用[J]. 广西师范大学学报(自然科学版), 2024, 42(6): 164-176.DOI: 10.16088/j.issn.1001-6600.2024020302.
[1] 曹锋, 王家帆, 易见兵, 李俊. 一种基于子句稳定度的多元动态演绎算法及应用[J]. 广西师范大学学报（自然科学版）, 2024, 42(6): 164-176.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] 田晟, 赵凯龙, 苗佳霖. 基于改进YOLO11n模型的自动驾驶道路交通检测算法研究[J]. 广西师范大学学报（自然科学版）, 2026, 44(1): 1 -9 .
[2] 唐程华, 易见兵, 吴欣, 熊文武, 王敬永. 跨域少样本图像语义分割方法综述[J]. 广西师范大学学报（自然科学版）, 2026, 44(4): 1 -27 .
[3] 田晟, 谢华林, 陈东. 基于改进深度强化学习的燃料电池汽车能量管理策略[J]. 广西师范大学学报（自然科学版）, 2026, 44(4): 28 -45 .
[4] 张旭, 刘迪迪. 基于TD3算法的电动汽车智能充/放电调度策略[J]. 广西师范大学学报（自然科学版）, 2026, 44(4): 46 -55 .
[5] 闫远洋, 谢丽蓉, 张龙军, 任娟, 黄晨晨, 胡超. 基于多目标优化的超短期风电功率预测模型[J]. 广西师范大学学报（自然科学版）, 2026, 44(4): 56 -70 .
[6] 陶振卓, 韦笃取. 参数未知永磁同步电机的自适应混沌同步控制[J]. 广西师范大学学报（自然科学版）, 2026, 44(4): 71 -78 .
[7] 王成龙, 宋强, 李文峰, 张仕民. PAM-DETR: 基于改进RT-DETR的医用手套小目标缺陷检测算法[J]. 广西师范大学学报（自然科学版）, 2026, 44(4): 79 -95 .
[8] 韦吴杰, 陈庆锋. 基于视图解耦与反事实增强的公平图学习[J]. 广西师范大学学报（自然科学版）, 2026, 44(4): 96 -106 .
[9] 罗珵, 黄文韬, 何东平, 张越. 一类具有十参数的复三次多项式微分系统的弱持续中心问题[J]. 广西师范大学学报（自然科学版）, 2026, 44(4): 121 -129 .
[10] 王展新, 韦煜明. 具有饱和发生率的确定性和随机SIS-SIRS传染病模型[J]. 广西师范大学学报（自然科学版）, 2026, 44(4): 130 -146 .
版权所有 © 广西师范大学学报（自然科学版）编辑部
地址：广西桂林市三里店育才路15号　邮编：541004
电话：0773-5857325　E-mail: gxsdzkb@mailbox.gxnu.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发