• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

Computer Engineering & Science ›› 2024, Vol. 46 ›› Issue (02): 374-380.

• Artificial Intelligence and Data Mining • Previous Articles    

Treelet-based graph neural network for premise selection in first-order logic

MA Xue1,HE Xing-xing1,LAN Yong-qi1,LI Ying-fang2   

  1. (1.School of Mathematics,Southwest Jiaotong University,Chengdu 611756; 
    2.School of Computing and Artificial Intelligence,Southwestern University of Finance and Economics,Chengdu 611130,China)
  • Received:2022-10-08 Revised:2023-03-23 Accepted:2024-02-25 Online:2024-02-25 Published:2024-02-26

Abstract: Premise selection is an efficient method to address the performance degradation of automated theorem provers when facing large-scale problems. Currently, the mainstream graph neural networks for premise selection in first-order logic ignore the node order information inside logic formula graphs. To solve the above problem, an order-preserving method for higher-order logical formulas is extended to first-order logic, and a treelet-based graph neural network model is proposed. The model aggregates the information of neighbor nodes in two parts: One part aggregates parent and child node information of the central node, the other part aggregates the order information of the central node. Experimental analysis shows that, compared with the optimal mainstream graph neural network model, the treelet-based graph neural network model improves the classification accuracy by about 2% in the premise selection task. 

Key words: first-order logical formula, graph neural network, premise selection, binary classification