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

Apr, 2024

本文提出了使用机器学习自动化证明助手交互的问题。研究人员通过构建 CoqGym 数据集和 ASTactic 模型，能够生成高效的策略程序并用于自动证明定理。

May, 2019

自动定理证明器和形式证明助手是理论上能够证明任意难题的一般推理系统，但在实践中面临组合爆炸所以包括很多启发式算法和选择点来影响系统性能。机器学习预测器可以引导这些推理系统的工作。本文概述了几个自动推理和定理证明领域及目前对它们进行的学习和人工智能方法，包括前提选择、证明引导、协同推理和学习的 AI 系统以及符号分类问题。

Mar, 2024

本文提出 HOL4 证明助手的机器学习辅助自动推理和前提选择方法，从定理陈述中提取特征选取前提，通过 HOLyHammer 将其转换为不同格式，再经由 ATPs 处理。实验显示该系统在 HOL4 标准库上具有较高的性能。

Sep, 2015

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

Oct, 2000

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

Dec, 2023

本篇论文基于 Isabelle-verified 事件结构枚举算法，通过对巨大数据库进行跨站数据挖掘，发现了连接看似不相关的数学对象（并发理论中的事件结构和计算生物学中的完整图）的新定理，并通过 Isabelle/HOL 定义和定理进行了形式验证，完成了 Isabelle-verified 事件结构枚举算法验证的全面验证框架以链接事件结构和完整图。

Jun, 2023

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

Apr, 2019

该研究结合学习与定理证明的多种方式显著提高了 E 自动定理证明器在 Isabelle Sledgehammer 问题上的性能，特别是在 ENIGMA 指导，神经前提选择和 E 的有针对性策略的开发方法上。最终的 ENIGMA 和前提选择系统在 15 秒内比 E 的最佳先前版本提高了 25.3％，也优于所有其他先前的 ATP 和 SMT 系统。该方法可在从 Isabelle 提取的数十万个一阶未分类和已分类问题的几次迭代训练中进行训练。

May, 2022

该论文表明，通过使用现有的证明助理，可以以与建立证明助理自身的信任和可审计性原则相一致的方式，构建对自然语言表达的规范的支持。我们在 Lean 证明助理内实现了一种方式，以可扩展的正式英语子集提供规范，并自动将其翻译成正式的命题。我们的方法是可扩展的（对语法结构没有永久限制），模块化的（允许在库中分发有关新词的信息），并且生成解释了每个词的解释方式以及如何使用句子结构来计算含义的证明证书。我们将原型应用于从一本流行教材中翻译各种正式规范的英文描述；在仅需进行小幅修改的情况下，借助一个适度的词汇表，所有规范都能被正确翻译。

Oct, 2023