• 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
TENG Fei, DAI Rongjie, REN Xiaochun. Parallel Algorithm for Overlapping Community Detection in Complex Networks[J]. Journal of Southwest Jiaotong University, 2019, 54(1): 211-218. doi: 10.3969/j.issn.0258-2724.20160478
Citation: 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

Edge-Weighted-Based Graph Neural Network for First-Order Premise Selection

doi: 10.3969/j.issn.0258-2724.20210134
  • Received Date: 23 Feb 2021
  • Rev Recd Date: 12 Jul 2021
  • Available Online: 24 Aug 2022
  • Publish Date: 17 Nov 2021
  • In order to improve the ability of automated theorem provers, the premise selection task emerges. Due to the directional nature of formula graphs, most current graph neural networks can only update nodes in one direction, and cannot encode the order of sub-nodes in the formula graph. To address the above problems, a bidirectional graph with edge types to represent logical formulae and a edge-weight-based graph neural network (EW-GNN) model to encode first-order logic formulae are proposed. The model firstly uses the information of connected nodes to update the feature representation of the corresponding edge type, then calculates the weight of the adjacent node to the central node with the updated edge type feature, and finally uses the information of the adjacent node to update the target node in both directions. The experimental results show the edge-weighted-based graph neural network model performs better in the premise selection task, which can improve the classification accuracy by 1% compared to the best model on the same test dataset.

     

  • [1]
    KERN C, GREENSTREET M R. Formal verification in hardware design: a survey[J]. ACM Transactions on Design Automation of Electronic Systems (TODAES), 1999, 4(2): 123-193. doi: 10.1145/307988.307989
    [2]
    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. Big Sky: ACM, 2009: 207-220.
    [3]
    LEROY X. Formal verification of a realistic compiler[J]. Communications of the ACM, 2009, 52(7): 107-115. doi: 10.1145/1538788.1538814
    [4]
    KOVÁCS L, VORONKO A. First-order theorem proving and vampire[C]//25th International Conference on Computer Aided Verification. Saint Petersburg: [s.n.], 2013: 1-35.
    [5]
    SCHULZ S. E – a brainiac theorem prover[J]. Ai Communications, 2002, 15(2/3): 111-126.
    [6]
    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
    [7]
    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
    [8]
    MCCUNE W W. Otter 3.0 reference manual and guide[R]. Chicago: Argonne National Lab., 1994.
    [9]
    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
    [10]
    HODER K, VORONKOV A. Sine qua non for large theory reasoning[C]//23th International Conference on Automated Deduction. Wroclaw: [s.n.], 2011: 299-314.
    [11]
    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
    [12]
    KALISZYK C, URBAN J, VYSKOČIL J. Efficient semantic features for automated reasoning over large theories[C]//Proceedings of the 24th International Conference on Artificial Intelligence. [S.l.]: AAAI Press, 2015: 3084-3090.
    [13]
    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.
    [14]
    ALEMI A A, CHOLLET F, EEN N, et al. DeepMath-deep sequence models for premise selection[C]// Proceedings of the 30th International Conference on Neural Information Processing Systems. Barcelona: Curran Associates Inc., 2016: 2243-2251.
    [15]
    WANG M, TANG Y, 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. Long Beach: Curran Associates Inc., 2017: 2783-2793.
    [16]
    CROUSE M, ABDELAZIZ I, CORNELIO C, et al. Improving graph neural network representations of logical formulae with subgraph pooling[EB/OL]. (2019-11-15). https://arxiv.org/abs/1911.06904.
    [17]
    PALIWAL A, LOOS S, RABE M, et al. Graph representations for higher-order logic and theorem proving[C]//34th Proceedings of the AAAI Conference on Artificial Intelligence. Palo Alto: AAAI Press, 2020: 2967-2974.
    [18]
    KIPF T N, WELLING M. Semi-supervised classification with graph convolutional networks[DB/OL]. (2016-09-09). https://doi.org/10.48550/arXiv.1609.02907.
    [19]
    VELIČKOVIĆ P, CUCURULL G, CASANOVA A, et al. Graph attention networks[DB/OL]. (2017-10-30). https://doi.org/10.48550/arXiv.1710.10903.
    [20]
    ROBINSON A J, VORONKOV A. Handbook of automated reasoning[M]. [S.l.]: Elsevier, 2001.
    [21]
    Rudnicki P. An overview of the Mizar project[C]//Proceedings of the 1992 Workshop on Types for Proofs and Programs. [S.l.]: Chalmers University of Technology, 1992: 311-330.
    [22]
    JAKUBŮVJ, URBAN J. ENIGMA: efficient learning-based inference guiding machine[C]//International Conference on Intelligent Computer Mathematics. Cham: Springer, 2017: 292-302.
    [23]
    COVER T, HART P. Nearest neighbor pattern classification[J]. IEEE Transactions on Information Theory, 1967, 13(1): 21-27.
    [24]
    PASZKE A, GROSS S, MASSA F, et al. PyTorch: an imperative style, high-performance deep learning library[DB/OL]. (2019-12-03). https://arxiv.org/abs/1912.01703
    [25]
    FEY M, LENSSEN J E. Fast graph representation learning with PyTorch geometric[DB/OL]. (2019-03-06). https://arxiv.org/abs/1903.02428
    [26]
    KINGMA D P, BA J. Adam: a method for stochastic optimization[DB/OL]. (2014-12-22). https://arxiv.org/abs/1412.6980.
    [27]
    HAMILTON W L, YING R, LESKOVEC J. Inductive representation learning on large graphs[C]//Proceedings of the 31st International Conference on Neural Information Processing Systems. Long Beach: [s.n.], 2017: 1025-1035.
    [28]
    WU F L, SOUZA A H, ZHANG T Y, et al. Simplifying graph convolutional networks[C]// International Conference on Machine Learning. [S.l.]: PMLR, 2019: 6861-6871.
    [29]
    DEFFERRARD M, BRESSON X, VANDERGHEYNST P. Convolutional neural networks on graphs with fast localized spectral filtering[C]//Proceedings of the 30th International Conference on Neural Information Processing Systems. Barcelona: [s.n.], 2016: 3844-3852.
  • Relative Articles

    [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]XU Xianze, SONG Mingxing, GONG Yongxing, XU Fengqiu, WANG Dijin, SUI Bowen, GUO Qingquan. Fractional-Order Sliding Mode Control for Maglev Rotary Table Based on Disturbance Compensation[J]. Journal of Southwest Jiaotong University, 2024, 59(4): 766-775. doi: 10.3969/j.issn.0258-2724.20230412
    [3]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
    [4]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
    [5]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
    [6]SUN Shibao, QIN Keyun. Construction Method of Fuzzy Concept Lattices Based on Residual Implication[J]. Journal of Southwest Jiaotong University, 2006, 19(2): 259-263.
    [7]PANXiao-dong, XU Yang, ZHANG Qing. Lattice Implication Algebraic Equations in Lattice Implication Algebras[J]. Journal of Southwest Jiaotong University, 2005, 18(6): 842-845.
    [8]WANG Wei, JIANG Bao-qing, XU Yang. α-Resolution Fields ofGeneralized Literals ofLogic LP(X)[J]. Journal of Southwest Jiaotong University, 2005, 18(4): 544-547.
    [9]QIN Ke-yun, TU Wen-biao. Rough Set Algebra and Lattice Implication Algebra[J]. Journal of Southwest Jiaotong University, 2004, 17(6): 754-757.
    [10]MAJun, GAO Ya, QINKe-yun, XUYang. Syntactic System of Lattice-Valued Propositional Logic Based on Finite Lattice Implication Algebra[J]. Journal of Southwest Jiaotong University, 2004, 17(1): 90-94.
    [11]WANG Qiong, HE Yi-nong, SONG Zhen-min. Sustaining Degree of Fuzzy Triple I Method Based on Residual Implication[J]. Journal of Southwest Jiaotong University, 2004, 17(4): 550-553.
    [12]WANG Wei, XUYang, QINKe-yun. The Topological Structure of Lattice Implication Algebras[J]. Journal of Southwest Jiaotong University, 2002, 15(3): 343-346.
    [13]PEI Zheng, HUANG Tian-min. Input Resolution on Horn Sets Based on Fuzzy Neural Networks[J]. Journal of Southwest Jiaotong University, 2002, 15(5): 565-569.
    [14]MAJun, QIN Ke-yun, XU Yang. Semantic System of Lattice-Valued Propositional Logic Based on Finite Lattice Implication Algebra[J]. Journal of Southwest Jiaotong University, 2002, 15(5): 557-560.
    [15]QIN Ke-yun, XU Yang. On Model Properties of Lattice Implication Algebra[J]. Journal of Southwest Jiaotong University, 2000, 13(5): 546-550.
    [16]Qin Keyun, Xu Yang. On Ultrafilters of Lattice Implication Algebras[J]. Journal of Southwest Jiaotong University, 1999, 12(1): 52-54.
  • Cited by

    Periodical cited type(1)

    1. 曹锋,谢燏,易见兵,李俊. 矛盾体分离单元结果演绎方法及应用. 计算机工程与科学. 2024(12): 2252-2260 .

    Other cited types(0)

  • Created with Highcharts 5.0.7Amount of accessChart context menuAbstract Views, HTML Views, PDF Downloads StatisticsAbstract ViewsHTML ViewsPDF Downloads2024-052024-062024-072024-082024-092024-102024-112024-122025-012025-022025-032025-0302.557.51012.5
    Created with Highcharts 5.0.7Chart context menuAccess Class DistributionFULLTEXT: 38.6 %FULLTEXT: 38.6 %META: 58.9 %META: 58.9 %PDF: 2.5 %PDF: 2.5 %FULLTEXTMETAPDF
    Created with Highcharts 5.0.7Chart context menuAccess Area Distribution其他: 8.5 %其他: 8.5 %其他: 0.2 %其他: 0.2 %China: 0.2 %China: 0.2 %上海: 0.9 %上海: 0.9 %东莞: 0.9 %东莞: 0.9 %临汾: 0.4 %临汾: 0.4 %保定: 0.2 %保定: 0.2 %保山: 0.9 %保山: 0.9 %克拉玛依: 0.2 %克拉玛依: 0.2 %北京: 2.9 %北京: 2.9 %南京: 3.1 %南京: 3.1 %南宁: 0.4 %南宁: 0.4 %台州: 0.4 %台州: 0.4 %合肥: 0.4 %合肥: 0.4 %哈尔滨: 0.2 %哈尔滨: 0.2 %哥伦布: 0.4 %哥伦布: 0.4 %唐山: 0.5 %唐山: 0.5 %太原: 0.4 %太原: 0.4 %宁波: 0.7 %宁波: 0.7 %宣城: 0.4 %宣城: 0.4 %常州: 0.4 %常州: 0.4 %延安: 0.4 %延安: 0.4 %开封: 0.2 %开封: 0.2 %张家口: 3.6 %张家口: 3.6 %成都: 1.1 %成都: 1.1 %昆明: 1.1 %昆明: 1.1 %昭通: 0.2 %昭通: 0.2 %晋城: 0.2 %晋城: 0.2 %杭州: 0.4 %杭州: 0.4 %武汉: 0.4 %武汉: 0.4 %江门: 0.2 %江门: 0.2 %池州: 0.4 %池州: 0.4 %沈阳: 0.9 %沈阳: 0.9 %洛阳: 0.7 %洛阳: 0.7 %深圳: 0.2 %深圳: 0.2 %湖州: 0.4 %湖州: 0.4 %漯河: 1.1 %漯河: 1.1 %珠海: 0.2 %珠海: 0.2 %石家庄: 0.9 %石家庄: 0.9 %秦皇岛: 0.2 %秦皇岛: 0.2 %芒廷维尤: 18.9 %芒廷维尤: 18.9 %芝加哥: 0.2 %芝加哥: 0.2 %莱芜: 0.2 %莱芜: 0.2 %衢州: 0.2 %衢州: 0.2 %西宁: 40.5 %西宁: 40.5 %西安: 0.2 %西安: 0.2 %贵阳: 0.2 %贵阳: 0.2 %邯郸: 0.2 %邯郸: 0.2 %郑州: 0.4 %郑州: 0.4 %重庆: 0.4 %重庆: 0.4 %长春: 0.4 %长春: 0.4 %长沙: 2.2 %长沙: 2.2 %青岛: 1.3 %青岛: 1.3 %其他其他China上海东莞临汾保定保山克拉玛依北京南京南宁台州合肥哈尔滨哥伦布唐山太原宁波宣城常州延安开封张家口成都昆明昭通晋城杭州武汉江门池州沈阳洛阳深圳湖州漯河珠海石家庄秦皇岛芒廷维尤芝加哥莱芜衢州西宁西安贵阳邯郸郑州重庆长春长沙青岛

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Figures(2)  / Tables(4)

    Article views(490) PDF downloads(36) Cited by(1)
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return