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

2020-09-06 18:12:33

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