ATWGNNS：用于前提选择的逻辑公式的简化表示与学习方法

《Artificial Intelligence》：ATWGNNS: Graph simplified representation and learning of logical formula for premise selection

　　

Xingxing He|Zhongxu Zhao|Yongqi Lan|Yingfang Li|Li Zou|Luis Martínez|Tianrui Li

摘要

前提选择有效解决了大理论定理证明中的挑战，其中图神经网络（GNNs）及其变体是常用的方法。相反，优化一阶逻辑中公式的图表示却很少被关注，尤其是在简化以及嵌入过程中保留的逻辑属性方面。本文提出了一种基于注意力机制的图神经网络（ATWGNNS），用于前提选择。首先，介绍了一种简化的公式图表示方法，该方法可以消除公式图中的重复量词。接下来，我们提出了衡量公式和图相似性的方法。实验表明，没有重复量词的图的相似性高于保留原始量词的其他图。此外，逻辑公式的相似性越高，相应图的相似性也越高。这证实了图表示方法的可解释性。最后，提出了一种基于注意力机制的图神经网络，用于在去除重复量词后保留简化公式图中的任务相关结构信息。实验结果表明，使用所提方法开发的模型在前提选择方面优于现有的最先进模型。