我们提供了一个基于 HOL Light 定理证明器的开源框架，可以用作强化学习环境；并提出了一个基于深度强化学习的自动定理证明器 DeepHOL，它在基准测试中取得了强大的初步结果。

Apr, 2019

开发了交互式定理证明器 Isabelle，以 Horn clause 表示每个推理规则，使用基于类型的 λ 演算表示逻辑语法，支持多个逻辑系统并具有逻辑编程潜能。

Oct, 2000

我们在 Isabelle 证明助手中对高阶逻辑进行了形式化处理，直接构建在 Isabelle/Pure 的基础框架上，旨在尽可能简洁易读，为对高阶逻辑和证明助手感兴趣但不想学习更复杂的 Isabelle/HOL 与较重自动化的人提供了良好的入门。通过展示我们的开发和方法，我们解释了一个样例证明，描述了高阶逻辑的公理和规则，并讨论了在课堂环境中教授这一主题的经验。

Apr, 2024

本文介绍了一种基于 Higher-Order Logic 证明的新数据集，旨在开发基于机器学习的定理证明策略并提出基于该数据集的各种机器学习任务，通过一些基于逻辑回归、卷积神经网络和循环神经网络的基准模型显示出将机器学习应用于 HOL 定理证明的前景。

Mar, 2017

提出了一种将抽象辩证框架及其语义编码为经典高阶逻辑的方法，通过证明助手 Isabelle/HOL 来正式编码并证明重要性质和语义关系。这种方法允许在统一逻辑环境中使用自动化和交互式推理工具对抽象辩证框架进行计算机辅助分析。示例应用包括形式分析和验证元理论性质以及在特定语义约束下生成解释和扩展。

Dec, 2023

本文首次使用图神经网络 (GNNs) 实现高阶证明搜索，并证明 GNNs 能够提高此领域的最新成果。我们考虑了高阶逻辑的几种图形表示，并将它们与 HOList 基准进行了评估。

May, 2019

本文探讨了构造基础数学的概念以及基于马丁 - 勒夫的含义阐释的构造类型理论，通过电脑程序语言提供了一种可行的理论意义解释并解释了更高维的类型理论，并提供了完整的计算公式以证明该理论。

Apr, 2016

该研究论文将 Agda 生态系统扩展到机器学习领域，并提供给机器学习从业者相关资源。作者发布了一个特殊的 Agda 程序证明数据集，该数据集详细且丰富，可以支持各种机器学习应用。基于数据集的超高分辨率，我们提出了一种新的神经网络架构，旨在以结构而非命名原则忠实地表示依赖类型程序。我们在前提选择设置中实例化并评估了我们的架构，取得了强有力的初步结果。

Feb, 2024

本研究介绍了反证完成的超位置演算法，用于意图性和外延句子 $\lambda$- 自由高阶逻辑，这两种形式允许部分应用和应用变量。 这些演算法由一个术语排序参数化，无需完全单调，从而可以采用 $\lambda$- 自由高阶词典路径和 Knuth-Bendix 排序。作者们在 Zipperposition prover 中实现了这些演算法，并在 Isabelle/HOL 和 TPTP 基准测试中评估它们。 它们似乎是通向完全高效自动定理证明程序的一个重要的步骤。

May, 2020

该论文提出了一种将概率论和第一阶逻辑相结合的方法，在有限域内具有 Herbrand 解释的情况下，定义了概率证明定理及其推广问题，然后提出了能够同时拥有图模型推理和一阶定理证明的完整能力的方法，并开发了一种高效算法。实验表明，当逻辑结构存在时，该算法远优于目前已有的方法。

Feb, 2012