• ISSN 0258-2724
  • CN 51-1277/U
  • EI Compendex
  • Scopus 收录
  • 全国中文核心期刊
  • 中国科技论文统计源期刊
  • 中国科学引文数据库来源期刊

基于符号权重的一阶逻辑前提选择方法

刘清华 李瑞杰 朱绪胜 陈代鑫

刘清华, 李瑞杰, 朱绪胜, 陈代鑫. 基于符号权重的一阶逻辑前提选择方法[J]. 西南交通大学学报, 2023, 58(3): 704-710. doi: 10.3969/j.issn.0258-2724.20220478
引用本文: 刘清华, 李瑞杰, 朱绪胜, 陈代鑫. 基于符号权重的一阶逻辑前提选择方法[J]. 西南交通大学学报, 2023, 58(3): 704-710. doi: 10.3969/j.issn.0258-2724.20220478
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
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

基于符号权重的一阶逻辑前提选择方法

doi: 10.3969/j.issn.0258-2724.20220478
基金项目: 国家自然科学基金(72101217)
详细信息
    作者简介:

    刘清华(1992—),女,工程师,博士,研究方向为自动推理,E-mail:qhliu@my.swjtu.edu.cn

    通讯作者:

    李瑞杰(1990—),男,讲师,博士,研究方向为智能控制,E-mail:ruijie-li@swjtu.edu.cn

  • 中图分类号: TP399

First-Order Logical Premise Selection Method Based on Symbol Weight

  • 摘要:

    为增强自动定理证明器从一阶逻辑问题的大规模前提中选择相关前提的能力,首先,提出符号权重计算公式,基于符号在问题中出现的频率获取不同符号对应的权重;其次,提出相关度计算公式,利用分配的符号权重计算问题中前提和结论间的相关度;同时,研究自适应相关度边界,用于判断前提与给定的结论是否相关;最后,在自动定理证明器中交互地结合前提选择和自动推理两个过程,可在充分选择相关前提的情况下及时停止前提选择过程. 实验结果表明:在最优情况下,新提出的前提选择方法能够把参与证明的平均前提数量从1876个降低到174个;与广泛使用的前提选择方法E-SInE和Vampire-SInE相比,使用新方法能够帮助自动定理证明器E在MPTP2078基准测试集上分别提高19.49%和10.49%的证明率.

     

  • 表  1  MPTP2078问题库描述

    Table  1.   Description of MPTP2078 benchmark

    项目公式结论最小前提最大前提平均前提符号
    数量456420781045631876784
    下载: 导出CSV

    表  2  参与实验的基于符号的前提选择方法的说明

    Table  2.   Description of symbol-based premise selection methods in experiments

    前提选择方法说明
    no-selection不使用任何前提选择
    SInE[19]基于触发关系的前提选择
    LightWeight[18]基于符号轻量相关性的前提选择
    SymbolWeight新提出的基于符号权重的前提选择
    下载: 导出CSV

    表  3  自动定理证明器E在SymbolWeight下的证明性能

    Table  3.   Performance of automated theorem prover E with SymbolWeight

    $ K $证明数
    量/个
    平均选择前提数量/个选择精
    确度
    选择度
    2 288 13.0 0.358 0.054
    4 599 22.6 0.336 0.060
    6 818 33.3 0.322 0.054
    8 862 44.5 0.309 0.053
    10 920 55.9 0.302 0.055
    12 932 68.4 0.295 0.057
    14 967 81.1 0.288 0.059
    16 980 94.0 0.285 0.060
    18 1003 106.3 0.280 0.061
    20 1014 117.3 0.278 0.061
    22 1028 128.7 0.275 0.064
    24 1045 140.7 0.271 0.068
    26 1057 151.5 0.268 0.070
    28 1071 162.4 0.265 0.074
    30 1077 174.2 0.264 0.076
    下载: 导出CSV

    表  4  自动定理证明器E在不同的基于符号的前提选择方法下的证明性能

    Table  4.   Performance of automated theorem prover E with different symbol-based premise selection methods

    前提选择方法证明数量/个证明率/%
    no-selection66330.90
    E-SInE67232.34
    Vampire-SInE85941.34
    SymbolWeight107751.83
    下载: 导出CSV
  • [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.
  • 加载中
表(4)
计量
  • 文章访问数:  275
  • HTML全文浏览量:  82
  • PDF下载量:  37
  • 被引次数: 0
出版历程
  • 收稿日期:  2022-07-12
  • 修回日期:  2023-03-14
  • 网络出版日期:  2023-05-05
  • 刊出日期:  2023-03-24

目录

    /

    返回文章
    返回