- ISSN 0258-2724
- CN 51-1277/U
- EI Compendex
- Scopus
- Indexed by Core Journals of China, Chinese S&T Journal Citation Reports
- Chinese S&T Journal Citation Reports
- Chinese Science Citation Database
| Citation: | ZENG Guoyan, XU Yang, CHEN Shuwei, JIANG Shipan. First-Order Logic Clause Selection Method Based on Multi-criteria Decision Making[J]. Journal of Southwest Jiaotong University, 2025, 60(1): 185-193. doi: 10.3969/j.issn.0258-2724.20230023
|
First-order logic-based automatic theorem provers (ATPs) are important for the research on knowledge representation and automatic reasoning, and heuristic strategies are a critical research topic to enhance the performance of ATPs. Mainstream heuristic strategies select clauses by describing clause properties and then determining the priority of the properties. However, the priority of properties is subject to human factors, and it takes a long time to evaluate clauses. A new multi-criteria decision making (MCDM) clause evaluation method was proposed based on the standard contradiction separation (S-CS) rule. Firstly, the entropy weight method was used to objectively assign weights to clause properties. Secondly, preference ranking organization method for enrichment evaluations (PROMETHEE Ⅱ) was combined to evaluate the clauses and obtain the complete order of the clauses. Finally, the proposed MCDM method was applied to ATPs CSE 1.5 (contradiction separation extension 1.5), Vampire 4.7, and Eprover (E 2.6) to form new ATPs MCDM_CSE, MCDM_V, and MCDM_E. The theorems in first-order form (FOF) from the international theorem provers problem library Thousands of Problems for Theorem Provers (TPTP) were tested on MCDM_CSE, and the Conference on Automated Deduction (CADE) 2022 competition (FOF division) was tested on MCDM_V and MCDM_E. The experiments show that MCDM_CSE proves 151 more theorems (from TPTP) than CSE 1.5 and proves 5 theorems unproved by Vampire 4.7, 41 theorems unproved by E 2.6, and 293 theorems unproved by Prover9. In a shorter average time, MCDM_V proves 6 more theorems (from CADE 2022) than Vampire 4.7, and MCDM_E proves 8 more theorems than E 2.6.
| [1] |
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
|
| [2] |
BECKERT B, HÄHNLE R. Reasoning and verification: state of the art and current trends[J]. IEEE Intelligent Systems, 2014, 29(1): 20-29. doi: 10.1109/MIS.2014.3
|
| [3] |
HALES T, ADAMS M, BAUER G, et al. A formal proof of the Kepler conjecture[J/OL]. Forum of Mathematics, Pi, 2017, 5:1-21. [2023-01-02]. https://arxiv.org/pdf/1501.02155.
|
| [4] |
PAVLOV V, SCHUKIN A, CHERKASOVA T. Exploring automated reasoning in first-order logic: tools, techniques and application areas[M]//Communications in Computer and Information Science. Berlin: Springer, 2013: 102-116.
|
| [5] |
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
|
| [6] |
XU Y, CHEN S W, LIU J, et al. Distinctive features of the contradiction separation based dynamic automated deduction[C]//Data Science and Knowledge Engineering for Sensing Decision Support. Belfast: World Scientific, 2018: 725-732.
|
| [7] |
JAKUBŮV J, KALISZYK C. Relaxed weighted path order in theorem proving[J]. Mathematics in Computer Science, 2020, 14(3): 657-670 doi: 10.1007/s11786-020-00474-0
|
| [8] |
RAWSON M, REGER G. Old or heavy? decaying gracefully with age/weight shapes[M]//Lecture Notes in Computer Science. Cham: Springer, 2019: 462-476.
|
| [9] |
曹锋,徐扬,陈树伟,等. 多元协同演绎在一阶逻辑ATP中的应用[J]. 西南交通大学学报,2020,55(2): 401-408,427. doi: 10.3969/j.issn.0258-2724.20180800
CAO Feng, XU Yang, CHEN Shuwei, et al. Application of multi-clause synergized deduction in first-order logic automated theorem proving[J]. Journal of Southwest Jiaotong University, 2020, 55(2): 401-408,427. doi: 10.3969/j.issn.0258-2724.20180800
|
| [10] |
CHEN S W, XU Y, JIANG Y, et al. Some synergized clause selection strategies for contradiction separation based automated deduction[C]//2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE). Nanjing: IEEE, 2017: 1-6.
|
| [11] |
HWANG C L, YOON K. Methods for multiple attribute decision making[M]//Lecture Notes in Economics and Mathematical Systems. Berlin: Springer, 1981: 58-191.
|
| [12] |
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
|
| [13] |
BRANS J P, VINCKE P. Note—a preference ranking organization method[J]. Management Science, 1985, 31(6): 647-656. doi: 10.1287/mnsc.31.6.647
|
| [14] |
BRANS J P, DE SMET Y. PROMETHEE methods[M]//HAMID F. International Series in Operations Research & Management Science. New York: Springer, 2016: 187-219.
|
| [15] |
ROBINSON J A, VORONKOV A. Handbook of automated reasoning[M]. Amsterdam: Elsevier, 2001.
|
| [16] |
LÖCHNER B. Things to know when implementing KBO[J]. Journal of Automated Reasoning, 2006, 36(4): 289-310.
|
| [17] |
TAMMET T. GKC: A reasoning system for large knowledge bases[C]//International Conference on Automated Deduction. Switzerland: Springer, 2019: 538-549.
|
| [18] |
RAWSON M, REGER G. Dynamic strategy priority: empower the strong and abandon the weak[C]// Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning. Oxford: PAAR, 2018: 58-71.
|
| [19] |
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
|
| [20] |
杨梦,雷博,史露娜,等. 基于标准离差法的模糊散度多阈值图像分割[J]. 计算机应用与软件,2020,37(5): 219-225. doi: 10.3969/j.issn.1000-386x.2020.05.038
YANG Meng, LEI Bo, SHI Luna, et al. Fuzzy divergence multi-threshold image segmentation based on standard deviation method[J]. Computer Applications and Software, 2020, 37(5): 219-225. doi: 10.3969/j.issn.1000-386x.2020.05.038
|
| [21] |
刘照德,詹秋泉,田国梁. 因子分析综合评价研究综述[J]. 统计与决策,2019,35(19): 68-73.
LIU Zhaode, ZHAN Qiuquan, TIAN Guoliang. Research review on comprehensive evaluation of factor analysis[J]. Statistics & Decision, 2019, 35(19): 68-73.
|
| [22] |
ZHU Y X, TIAN D Z, YAN F. Effectiveness of entropy weight method in decision-making[J]. Mathematical Problems in Engineering, 2020, 2020: 3564835.1-3564835.5.
|
| [23] |
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: 8851684.1-8851684.13.
|
| [24] |
ZHONG J, CAO F, WU G F, et al. Multi-clause synergized contradiction separation based first-order theorem prover—MC-SCS[C]//2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE). Nanjing: IEEE, 2017: 1-6.
|
| [25] |
SUTCLIFFE G, DESHARNAIS M. The CADE-28 automated theorem proving system competition–CASC-28[J]. AI Communications, 2022, 34(4): 259-276. doi: 10.3233/AIC-210235
|
| [26] |
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
|
| [27] |
KOVÁCS L, VORONKOV A. First-order theorem proving and vampire[M]//Lecture Notes in Computer Science. Berlin: Springer, 2013: 1-35.
|
| [28] |
SCHULZ S. System description: E 1.8[C]//International Conference on Logic for Programming Artificial Intelligence and Reasoning. Berlin: Springer, 2013: 735-743.
|
| [29] |
MCCUNE W. Release of Prover9[R]//Denver: Mathematics and Computer Science Division, Argonne National Laboratory, 2005.
|
| [30] |
MCCUNE W. OTTER 3.3 reference manual[J]. Office of Scientific & Technical Information Technical Reports, 2007, 11(4): 217-220.
|
| [1] | CUI Hongchao, HAN Shida, LI Chen, ZHANG Jiajia, LI Decai. Design of Automatic Flotation Separation Structure Based on First-Order Buoyancy of Magnetic Liquids[J]. Journal of Southwest Jiaotong University, 2023, 58(4): 947-956. doi: 10.3969/j.issn.0258-2724.20210723 |
| [2] | LIU Qinghua, LI Ruijie, ZHU Xusheng, CHEN Daixin. First-Order Logical Premise Selection Method Based on Symbol Weight[J]. Journal of Southwest Jiaotong University, 2023, 58(3): 704-710. doi: 10.3969/j.issn.0258-2724.20220478 |
| [3] | LIU Qinghua, XU Yang, WU Guanfeng, LI Ruijie. Edge-Weighted-Based Graph Neural Network for First-Order Premise Selection[J]. Journal of Southwest Jiaotong University, 2022, 57(6): 1368-1375. doi: 10.3969/j.issn.0258-2724.20210134 |
| [4] | CAO Feng, XU Yang, CHEN Shuwei, WU Guanfeng, CHANG Wenjing. Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving[J]. Journal of Southwest Jiaotong University, 2020, 55(2): 401-408, 427. doi: 10.3969/j.issn.0258-2724.20180800 |
| [5] | NING Xinran, XU Yang, HE Xingxing. Extended Unifying Principle of Clause Elimination in First-Order Logic[J]. Journal of Southwest Jiaotong University, 2020, 55(3): 588-595. doi: 10.3969/j.issn.0258-2724.20180974 |
| [6] | WANG Chao, ZHU Ming, ZHAO Yuandi. Air Traffic Flow Prediction Model Based on Improved Adding-Weighted One-Rank Local-rejion Method[J]. Journal of Southwest Jiaotong University, 2018, 53(1): 206-213. doi: 10.3969/j.issn.0258-2724.2018.01.025 |
| [7] | CHEN Qingshan, XU Yang, HE Xingxing. Heuristic Complete Algorithm for SAT Problem by Using Logical Deduction[J]. Journal of Southwest Jiaotong University, 2017, 30(6): 1224-1232. doi: 10.3969/j.issn.0258-2724.2017.06.025 |
| [8] | XU Tao, DING Xiaolu, LI Jianfu. K-Multiple Constrained Shortest Paths Problem for Connecting Path Search in International Flight Path Network[J]. Journal of Southwest Jiaotong University, 2014, 27(1): 153-159. doi: 10.3969/j.issn.0258-2724.2014.01.024 |
| [9] | MA Liang, GUO Jin, CHEN Guangwei. Constraint Propagation and Heuristics Backtracking Algorithm for Static Wagon-Flow Allocation at a Marshalling Station[J]. Journal of Southwest Jiaotong University, 2014, 27(6): 1116-1122. doi: 10.3969/j.issn.0258-2724.2014.06.027 |
| [10] | CHEN Jingrong, YU Jianning, LI Yinzhen. Path Optimization in Stochastic and Time-Dependent Networks with Multi-attributes[J]. Journal of Southwest Jiaotong University, 2012, 25(2): 291-298. doi: 10.3969/j.issn.0258-2724.2012.02.020 |
| [11] | YOU Houxing, LIN Jie. Multi-attribute Group Decision-Making Method for Interval Number Decision Information[J]. Journal of Southwest Jiaotong University, 2012, 25(4): 712-718. doi: 10.3969/j.issn.0258-2724.2012.04.028 |
| [12] | FENG Chao, YUAN Chao-Wei. Optimization of Kernel Parameters Based on Third-Order Rényi Entropy[J]. Journal of Southwest Jiaotong University, 2011, 24(6): 899-903. doi: 10.3969/j.issn.0258-2724.2011.06.002 |
| [13] | ZHANG Jianyong, LI Jun, GUO Yaohuang. Insertion Heuristic Algorithm for Dynamic Vehicle Routing Problem with Fuzzy Due-Time[J]. Journal of Southwest Jiaotong University, 2008, 21(1): 107-113. |
| [14] | WANG Xiaoyong, TANG Dunbing, LOU Peihuang. Multi-attribute Decision-Making Method Based on Design Axioms[J]. Journal of Southwest Jiaotong University, 2008, 21(3): 392-397. |
| [15] | GUO Hongling, HUANG Dingxuan. Weight Integration Method without Preference on Multi-attribute Decision Making[J]. Journal of Southwest Jiaotong University, 2007, 20(4): 505-510. |
| [16] | GUO Yao-huang, GUO Chun-xiang, GUO Qiang. Multiple Criteria Decision-Making Based on Similarity Degree Between Partial Orders[J]. Journal of Southwest Jiaotong University, 2006, 19(1): 1-6. |
| [17] | JIANMing, HUANG Ding-xuan, WUZhen-ye. W eight Syncretizing forMultiattribute Decision- M aking withoutDecision Attribute[J]. Journal of Southwest Jiaotong University, 2005, 18(2): 264-268. |
| [18] | PENG Yi, HU Yang, GUO Yao-huang. Multi-attribute Group Decision-Making Algorithm Based on Group s Ideal Solution[J]. Journal of Southwest Jiaotong University, 2003, 16(6): 682-685. |
| [19] | LIBing, YEHuai-zhen. A Heuristic Layout Restriction Algorithm for Solving Two-Dimensional Rectangular Layout Loading Problems[J]. Journal of Southwest Jiaotong University, 2002, 15(4): 443-447. |
| [20] | XIEBing-lei, LIJun, LIUJian-xin. A Heuristic Genetic Algorithm for the Travelling Salesman Problem with Time Restraints[J]. Journal of Southwest Jiaotong University, 2001, 14(2): 211-213. |
| 1. | 曹锋，杨小玲，易见兵，李俊. 基于子句正负文字的多元演绎算法. 华中科技大学学报(自然科学版). 2025(05): 157-163 .  |
Figures(3) / Tables(4)
ZENG Guoyan, XU Yang, CHEN Shuwei, JIANG Shipan. First-Order Logic Clause Selection Method Based on Multi-criteria Decision Making[J]. Journal of Southwest Jiaotong University, 2025, 60(1): 185-193. doi: 10.3969/j.issn.0258-2724.20230023
DownLoad:
