Premise selection is an efficient method to address the performance degradation of automa-ted theorem provers when facing large-scale problems.Currently,the mainstream graph neural net-works 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 ex-tended to first-order logic,and a treelet-based graph neural network model is proposed.The model ag-gregates the information of neighbor nodes in two parts:One part aggregates parent and child node in-formation of the central node,the other part aggregates the order information of the central node.Ex-perimental 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.
维普
万方数据