- 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.
|
DownLoad: