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