- 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: | 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
|
To enhance the ability of automated theorem provers to select relevant premises from large-scale premises of first-order logic problems, a symbol weight calculation formula is first proposed, obtaining various weights corresponding to different symbols based on the frequency of symbols in the problem. Secondly, the correlation calculation formula is proposed, using assigned symbol weights to compute the correlation between a premise and the conjecture in a problem. At the same time, the adaptive correlation boundary is studied, which is used to determine whether the premise is correlated with the given conjecture. Finally, both processes of premise selection and automated reasoning are interactively combined in automated theorem provers, achieving the goal of stopping the premise selection process in time when the relevant premises are fully selected. The experimental results show that in the optimal case, the proposed premise selection method can reduce the average number of premises involving in proving process from 1876 to 174, and compared with widely used premise selection methods E-SInE and Vampire-SInE in automated theorem provers, the propoed method can help the automated theorem prover E improve the proof rate by 19.49% and 10.49% respectively on the MPTP2078 benchmark.
| [1] |
DARWICHE A. Compiling knowledge into decomposable negation normal form[C]//Proceedings of the Sixteenth International Joint Conference on Artifical Intelligence. New York: ACM, 1999: 284-289.
|
| [2] |
KERN C, GREENSTREET M R. Formal verification in hardware design: a survey[J]. ACM Transactions on Design Automation of Electronic Systems, 1999, 4(2): 123-193. doi: 10.1145/307988.307989
|
| [3] |
JACKSON D, SCHECHTER I, SHLYAHTER H. Alcoa: the alloy constraint analyzer[C]//Proceedings of the 22nd International Conference on Software Engineering. New York: ACM, 2000: 730-733.
|
| [4] |
LEROY X. Formal verification of a realistic compiler[J]. Communications of the ACM, 2009, 52(7): 107-115.
|
| [5] |
KLEIN G, ELPHINSTONE K, HEISER G, et al. seL4: Formal verification of an OS kernel[C]//Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. New York: ACM, 2009: 207-220
|
| [6] |
KAUTZ H, SELMAN B. Planning as satisfiability[C]// Proceedings of the 10th European Conference on Artificial Intelligence. New York: ACM, 1992: 359-363.
|
| [7] |
RINTANEN J, HELJANKO K, NIEMELÄ I. Planning as satisfiability: parallel plans and algorithms for plan search[J]. Artificial Intelligence, 2006, 170(12/13): 1031-1080.
|
| [8] |
LARRABEE T. Test pattern generation using boolean satisfiability[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1992, 11(1): 4-15. doi: 10.1109/43.108614
|
| [9] |
WOOD R G, RUTENBAR R A. FPGA routing and routability estimation via Boolean satisfiability[J]. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 1998, 6(2): 222-231. doi: 10.1109/92.678873
|
| [10] |
EGGERSGLUSS S, DRECHSLER R. Efficient data structures and methodologies for SAT-based ATPG providing high fault coverage in industrial application[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2011, 30(9): 1411-1415. doi: 10.1109/TCAD.2011.2152450
|
| [11] |
CLARKE E, KROENING D, LERDA F. A tool for checking ANSI-C programs[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springe, 2004: 168-176.
|
| [12] |
LENAT D. CYC: a large-scale investment in knowledge infrastructure[J]. Communications of the ACM, 1998, 38(11): 33-38.
|
| [13] |
NILES I, PEASE A. Towards a standard upper ontology[C]//Proceedings of the international conference on Formal Ontology in Information Systems. New York: ACM, 2001: 2-9.
|
| [14] |
KALISZYK C, URBAN J. MizAR 40 for mizar 40[J]. Journal of Automated Reasoning, 2015, 55(3): 245-256. doi: 10.1007/s10817-015-9330-8
|
| [15] |
SUTCLIFFE G, PUZIS Y. SRASS-A semantic relevance axiom selection system[C]//International Conference on Automated Deduction. Berlin: Springer, 2007: 295-310.
|
| [16] |
PUDLÁK P. Semantic selection of premisses for automated theorem proving[C]//Cade-21 Workshop on Empirically Successful Automated Reasoning in Large Theories. Bremen: [s.n.], 2007: 1-18.
|
| [17] |
ROEDERER A, PUZIS Y, SUTCLIFFE G. Divvy: an ATP meta-system based on axiom relevance ordering[C]//International Conference on Automated Deduction. Berlin: Springer, 2009: 157-162.
|
| [18] |
MENG J, PAULSON L C. Lightweight relevance filtering for machine-generated resolution problems[J]. Journal of Applied Logic, 2009, 7(1): 41-57. doi: 10.1016/j.jal.2007.07.004
|
| [19] |
HODER K, VORONKOV A. Sine Qua Non for large theory reasoning[C]//International Conference on Automated Deduction. Berlin: Springer, 2011: 299-314.
|
| [20] |
ALAMA J, HESKES T, KÜHLWEIN D, et al. Premise selection for mathematics by corpus analysis and kernel methods[J]. Journal of Automated Reasoning, 2014, 52(2): 191-213. doi: 10.1007/s10817-013-9286-5
|
| [21] |
KALISZYK C, URBAN J, VYSKOCIL J. Efficient semantic features for automated reasoning over large theories[C]//Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Palo Alto: AAAI Press, 2015: 3084-3090.
|
| [22] |
PIOTROWSKI B, URBAN J. ATPboost: learning premise selection in binary setting with ATP feedback[C]//International Joint Conference on Automated Reasoning. Cham: Springer, 2018: 566-574.
|
| [23] |
IRVING G, SZEGEDY C, ALEMI A A, et al. Deep-math−deep sequence models for premise selection[C]// Proceedings of the 30th International Conference on Neural Information Processing Systems. New York: Curran Associates Inc. , 2016: 2243-2251.
|
| [24] |
WANG M Z, TANG Y H, WANG J, et al. Premise selection for theorem proving by deep graph embedding[C]//Proceedings of the 31st International Conference on Neural Information Processing Systems. New York: ACM, 2017: 2787-2797.
|
| [25] |
CROUSE M, ABDELAZIZ I, CORNELIO C, et al. Improving graph neural network representations of logical formulae with subgraph pooling[C]// KDD’20 Deep Learning on Graphs Workshop. San Diego: [s.n.], 2019: 1-7.
|
| [26] |
LIU Q H, XU Y, HE X X. Attention recurrent cross-graph neural network for selecting premises[J]. International Journal of Machine Learning and Cybernetics, 2022, 13(5): 1301-1315. doi: 10.1007/s13042-021-01448-9
|
| [27] |
刘清华,徐扬,吴贯锋,李瑞杰. 基于边权重图神经网络的一阶逻辑前提选择[J]. 西南交通大学学报,2022,57(6): 1368-1375. doi: 10.3969/j.issn.0258-2724.20210134
LIU Q H, XU Y, WU G F, et al. Edge-eighted-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
|
| [28] |
HARRISON J. Handbook of practical logic and automated reasoning[M]. Cambridge: Cambridge University Press, 2009.
|
| [29] |
LIU Q H, WU Z S, WANG Z H, et al. Evaluation of axiom selection techniques[C]// 10th International Joint Conference on Automated Reasoning. Paris: CEUR-WS, 2020: 63-75.
|
| [1] | 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 |
| [2] | 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 |
| [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] | ZHOU Yong, ZHU Wujia. Answer Set Semantics for Ordered Logic Programs[J]. Journal of Southwest Jiaotong University, 2006, 19(2): 163-167. |
| [8] | TONG Ji-xian. Distribution Theorem s for Values ofPower Functions with Complex Bases and Exponents[J]. Journal of Southwest Jiaotong University, 2005, 18(6): 829-831. |
| [9] | LIUWen-li. Nernst Theorem and Entropy ofTwo DimensionalBlack Holes[J]. Journal of Southwest Jiaotong University, 2005, 18(4): 558-561. |
| [10] | DU Wei-feng, SUN Shi-bao. On the Representation Theorems of Fuzzy Rough Sets[J]. Journal of Southwest Jiaotong University, 2005, 18(1): 118-121. |
| [11] | SHIQi-kai, SHIKai-ge. New Viewpoint of Dissecting Bertrand s Paradox —Analysis of CournotModel withModified Hypotheses[J]. Journal of Southwest Jiaotong University, 2004, 17(2): 248-252. |
| [12] | Automated ReasoningMethod Based on Path Searching for Lattice Propositional Logic Formulae[J]. Journal of Southwest Jiaotong University, 2003, 16(3): 248-252. |
| [13] | GUO Yao-huang, LIUJia-cheng, ZHOUWen-kun. Axioms for Lattice Ordered Decision-Making Behavior and Relative Utility Theorem[J]. Journal of Southwest Jiaotong University, 2001, 14(3): 221-224. |
| [14] | TIANJun, PENGJian-hua. A Global Saturation Theorem for the Mixed Exponential Type Integral Operators[J]. Journal of Southwest Jiaotong University, 2000, 13(4): 430-433. |
| [15] | PEI Dao-wu, WANG Guo-jun. A New Kind of Algebraic Systems for Fuzzy Logic[J]. Journal of Southwest Jiaotong University, 2000, 13(5): 564-568. |
| 1. | 高纯杰，何婷，张海龙，时小倩. 分布式结构的主—分控集控站群设计及实现. 微型电脑应用. 2025(03): 308-312 .  |
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
DownLoad: