高阶逻辑的图表示与定理证明(2019)

下载PDF摘要：本文首次使用图神经网络(GNN)进行高阶证明搜索，并证明了GNN可以改善该领域最先进的结果。交互式的高阶定理证明器允许大多数数学理论的形式化，并已被证明对深度学习构成了巨大的挑战。高阶逻辑具有很强的表现力，尽管它结构良好，语法和语义定义清晰，但仍然没有成熟的方法将公式转换为基于图形的表示。在这篇文章中，我们考虑了几种高阶逻辑的图形表示，并对照HOList基准对它们进行了评估，以用于高阶定理证明。