Machine-Checked Categorical Diagrammatic Reasoning
本文基于 Coq 构建面向 1-范畴图表证明的形式化证明库，通过深度嵌入的领域特定语言和专用证明命令，自动完成并检验文献中常被略去的技术推理。
2024-02-29 cs.LO
Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library
本研究提出HOLMS这一HOL Light中的模态推理模块化框架，开发了证明多类正规模态系统关系语义适当性的统一策略，集成自动化决策程序与反模型构造器，验证了模态推理机械化的可行性。
2025-06-11 cs.LO math.LO
Experiences from Exporting Major Proof Assistant Libraries
证明助手的互操作性及其库的集成是定理证明领域中一个非常有价值但难以实现的目标。作为准备步骤，在之前的工作中，我们将多个证明助手的库，特别是Coq、HOL Light、IMPS、Isabelle、Mizar和PVS的库转换为通用格式：OMDoc/MMT。每一种翻译都提出了巨大的理论、技术和社会挑战，有些是普遍的，有些是系统特定的，有些是可以解决的，有些仍然是开放的。在本文中，我们调查这些挑战，并比较和评估我们选择的解决方案。我们相信，类似的库翻译将是任何未来系统互操作性解决方案的重要组成部分，我们的经验将证明对其他从事此类工作的人有价值。
2020-05-05 cs.LO cs.SE
The Agda Universal Algebra Library, Part 2: Structure
Agda Universal Algebra Library（UALib）是我们开发的类型和程序（定理和证明）库，用于使用Agda程序设计语言和证明助手形式化依赖类型论中的通用代数基础。UALib包含了来自泛代数、方程逻辑和模型理论的大量定义、定理和证明，并提供了许多例子，展示了归纳和依赖类型在表示和推理数学结构和方程理论方面的能力。在本文中，我们描述的类型和证明的UALib涉及同态，项，和子代数。
2021-03-16 cs.LO math.LO
The Agda Universal Algebra Library, Part 1: Foundation
Agda Universal Algebra Library（UALib）是我们开发的类型和程序（定理和证明）库，用于使用Agda程序设计语言和证明助手形式化依赖类型论中的通用代数基础。UALib包含了大量的定义、定理和来自一般代数和方程逻辑的证明，包括许多展示归纳和依赖类型的能力的例子，用于表示和推理关系、代数结构和方程理论。在本文中，我们将讨论的逻辑基础上建立的图书馆，并描述了类型定义的前13个模块的图书馆。特别注意的是，从类型论或数学基础的角度来看，图书馆似乎最有趣或最具挑战性的方面。
2021-04-20 cs.LO math.LO
Homotopy Type Theory in Lean
我们在精益证明助手中讨论同伦类型论库。该图书馆特别面向合成同伦理论。特别令人感兴趣的是使用了一些高级归纳类型的原始概念，即截断和截断，以及立方方法的使用。
2017-09-20 cs.LO math.LO
Certified Exact Transcendental Real Number Computation in Coq
提出在Coq证明助手中实现基于完备度量空间的精确实数计算库，并开发自动证明闭基本实数表达式严格不等式的策略。
2008-05-16 cs.LO cs.MS cs.NA
Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT)
Refinement Reflection通过将实现用户定义函数的代码反映到函数的（输出）细化类型中，将您最喜欢的程序设计语言变成一个证明助手。因此，在函数的使用中，函数定义以精确的、可预测的、最重要的是程序员可控的方式展开到细化逻辑中。在逻辑中，我们使用未解释的符号编码的功能，并保留基于SMT的可判定性验证。在该语言中，我们提供了一个组合子库，让程序员可以从基本的改进和函数定义中组合证明。我们已经在Liquid Haskell系统中实现了我们的方法，从而将Haskell转换为一个交互式证明助手，我们用来验证各种属性，从高阶的算术属性，递归函数到Monoid，Application，Functor和Monad类型的类法律的各种实例。
2016-10-14 cs.LO cs.PL
Formalized Haar Measure
给出了Lean定理证明器中Haar测度存在唯一性的形式化证明。Haar测度是局部紧群上的一个不变正则测度，它在证明助手中还没有被形式化.我们还将讨论Lean的数学库\textsf{mathlib}中的测度理论库，并讨论乘积测度的构造和Bochner积分的Fubini定理的证明。
2021-02-04 cs.LO math.FA
Matching concepts across HOL libraries
许多证明助手库包含相同数学概念的形式化。这些概念通常以不同的方式引入（定义），但它们所具有的属性以及相应的形式化是相同的。对于基本概念，比如自然数，由于数学命名约定，在库之间匹配它们通常很简单。然而，对于更高级的概念，即使对于专家来说，在不同的库中找到类似的形式化也是一项重要的任务。在本文中，我们研究了自动发现的相似概念，跨图书馆的证明助手。我们提出了一种规范化的正式图书馆和一些相似性措施的概念属性的方法。我们在基于HOL的证明助手HOL 4、HOL Light和Isabelle/HOL上对该方法进行了评估，发现了398对同构常数和类型。
2014-05-15 cs.LO
A bi-directional extensible interface between Lean and Mathematica
我们实现了一个用户可扩展的特设精益证明助手和计算机代数系统Mathematica之间的连接。通过在另一个系统中反映每个系统的语法，并为扩展翻译提供灵活的接口，我们的连接允许在两个系统之间交换任意信息。我们展示了如何利用精益元编程框架来验证某些Mathematica计算，这样证明助手的严谨性就不会受到影响。我们还使用Mathematica作为一个不受信任的oracle来指导证明助手中的证明搜索，并在精益会话中与Mathematica笔记本进行交互。在另一个方向上，我们从Mathematica中导入并处理精益声明。证明助手库作为CAS可以显示和探索的数学知识数据库。
2021-01-17 cs.LO cs.MS
Translating HOL to Dedukti
Dedukti是一个基于Pudda-Pi-calculus模重写的逻辑框架，它扩展了Pudda-Pi-calculus的重写规则。在本文中，我们展示了如何将一个家庭的HOL证明助手的证明Dedukti。翻译保留了绑定、键入和缩减。我们在一个自动化工具中实现了这种翻译，并使用它成功地翻译了OpenTheory标准库。
2015-07-31 cs.LO
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
证明助手经常调用自动定理证明器来证明子目标。然而，每个证明器都有自己的证明演算，它产生的证明轨迹往往缺乏许多细节来构建完整的证明。因此，这些痕迹很难检查和重用的证明助手。Dedukti是一个证明检查器，其证明可以翻译为各种证明助手：Coq，HOL，Lean，Matita，PVS。我们实现了一个工具，从TSTP文件中提取TPTP子问题，并使用能够生成Dedukti证明的自动证明器（如ZenonModulo或ArchSAT）在Dedukti中重建完整的证明。此工具是通用的：它不假设证明器产生跟踪的证明演算，并且它可以使用不同的证明器来产生Dedukti证明。我们将我们的工具应用于TPTP库的CNF问题上的自动定理证明器产生的痕迹，并且我们能够为其中的大部分重建证明，显着增加了可以为这些问题获得的Dedukti证明的数量。
2019-08-26 cs.LO
Ackermann's Function in Iterative Form: A Proof Assistant Experiment
阿克曼函数可以使用迭代算法来表示，其基本上采用项重写系统的形式。虽然这种算法的终止是远远不明显的，它的等价性，传统的递归公式-因此，它的整体-有一个简单的证明在伊莎贝尔/HOL。这是一个使用证明助手形式化数学的小例子，重点是处理困难的递归。
2021-08-13 cs.LO
A Machine-checked proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory
Agda Universal Algebra Library（agda-algebras）是我们开发的类型和程序（定理和证明）库，用于使用Agda程序设计语言和证明助手在依赖类型论中形式化通用代数的基础。在本文中，我们借鉴和解释许多组件的agda代数库，我们提取到一个单一的Agda模块，以提出一个自包含的形式和建设性的证明Birkhoff的HSP定理在马丁-洛夫依赖类型论。在我们的演讲过程中，我们强调了一些更具挑战性的方面，形式化的基本定义和定理的通用代数类型论。尽管如此，我们希望这篇论文和agda代数库可以作为进一步的证据来支持这样一个主张，即依赖类型论和Agda语言，尽管它们对用户提出了技术要求，但对于那些拥有足够耐心和决心用证明助手正式验证其结果的工作数学家（比如我们自己）来说，是可以访问的。事实上，agda-algebras库现在包括了大量的定义、定理和泛代数的证明，说明了归纳和依赖类型在表示和推理一般代数和关系结构方面的表达能力。
2021-11-30 cs.LO math.LO
Design and Implementation of the Andromeda Proof Assistant
Andromeda是一个LCF风格的证明助手，用户通过用元级程序设计语言AML编写代码来构建可导出的判断。Andromeda唯一可信的组件是一个最小化的核心（对象级类型论的推理规则的实现），它控制类型论判断的构造和分解。由于nucleus不执行复杂的任务，如语法相等之外的相等性检查，这个责任被委托给用户，用户在元语言中实现一个或多个相等性检查过程。AML解释器使用代数操作和处理程序的机制从用户代码中请求相等的见证。核心中的动态检查保证不会构造无效的对象级派生。%，即使AML代码（或解释器）是不可信的。为了证明这种系统结构的灵活性，我们实现了一个核心组成的依赖类型论与平等的反射。等式反射提供了非常高的表达能力，因为它允许用户添加新的判断等式，但它也破坏了类型论的理想元理论属性（例如可判定性和强规范化）。AML中的效果和处理程序的强大功能通过一个标准库来展示，该库提供了用于相等性检查、范式计算和隐式参数填充的默认算法。用户可以通过提供本地“提示”或完全替换这些算法来扩展这些新算法。我们证明了由此产生的系统，展示了如何公理化和计算自然数，公理化的无类型的$λ$-演算，并通过实现一个简单的自动化系统，用于管理宇宙的类型。
2018-02-17 cs.LO
Verified Real Number Calculations: A Library for Interval Arithmetic
在机械证明中，初等函数的实数计算是非常困难的。在本文中，我们将展示如何在一个定理证明器或证明助手中以一种方便、高度自动化和交互式的方式进行这些计算。首先，我们正式建立了初等函数的上界和下界。然后，基于这些界限，我们开发了一个合理的区间算术实数计算发生在代数设置。为了减少区间算术的依赖效应，我们结合了两种技术：区间分裂和泰勒级数展开。这种务实的方法已经开发，并正式验证，在定理证明。正式的开发还包括一组可定制的策略，以自动化涉及实数显式计算的证明。我们的最终目标是提供有保证的数值性质的证明与最小的人类定理证明者的相互作用。
2007-08-28 cs.LO cs.MS
Mechanized HOL Reasoning in Set Theory
本文提出将高阶逻辑与代数数据类型嵌入到带ZFC公理的一阶逻辑中，在Lisa证明助手中实现，支持顶层多态性和ADT，并提供集合论中函数推理工具。
2024-03-20 cs.LO
Experience Implementing a Performant Category-Theory Library in Coq
我们描述了我们的经验，实现了广泛的范畴论库在Coq。范畴论和计算性能通常不会被相提并论，但我们需要大量的工程努力来教Coq处理大型范畴结构，而不会令人无法接受地减慢证明脚本处理。在本文中，我们分享了我们所学到的关于如何在Coq中表示非常抽象的数学对象和参数的经验教训，以及如何设计未来的证明助手来更好地支持这种推理。一个特殊的编码技巧，我们提请注意允许范畴理论的论点，涉及对偶性内在的柯克的逻辑与定义的平等。我们的可能是迄今为止最大的Coq开发，使用同伦类型理论家开发的相对较新的Coq版本，我们反思哪些新功能特别有用。
2014-04-18 cs.LO math.CT
Reconstructing veriT Proofs in Isabelle/HOL
自动定理证明器现在通常用于交互式定理证明器中，以履行越来越多的证明义务。为了保持证明的可信度，必须在证明助手中验证自动找到的证明。我们在这里提出了一个重建过程中的证明助手Isabelle/HOL证明生成的可满足性模理论求解器veriT这是smt策略的一部分。我们详细描述了我们改进的重建方法的架构和我们在设计它时所面临的挑战。我们的实验表明，VeriT驱动的SMT策略经常被Sledgehammer建议为自动解决证明目标的最快方法。
2019-08-26 cs.LO
A Coq Library of Sets for Teaching Denotational Semantics
本文提出一个基于 Coq 类型类系统的集合与关系库，用标准数学记号改善指称语义教学中的可读性，同时保持零证明项开销。
2024-04-08 cs.LO cs.PL
Isabelle/HOL as a Meta-Language for Teaching Logic
证明助手是逻辑教学的重要工具。我们支持这一主张，讨论三个形式化的Isabelle/HOL在最近的课程中使用的自动推理。第一个是系统W（一个只有两个原始符号的经典命题逻辑系统）的形式化，第二个是自然演绎助手（NaDeA），第三个是使用我们的序列演算验证器（SeCaV）的单边递归演算。我们依次描述每个形式化，集中在我们如何在教学中使用它们，并从逻辑教育的角度评论有趣或有用的功能。最后，我们反思了所吸取的经验教训，以及这些经验教训下一步可能引导我们走向何方。
2020-10-30 cs.LO
Developments in Formal Proofs
这份报告描述了三个特殊的技术进步，在正式的证明。HOL光证明助手将被用来说明一个高度可靠的系统的设计。今天，证明助手可以验证大量的高等数学;作为一个例子，我们转向群论中费特-汤普森奇阶定理的Coq形式证明。最后，我们讨论了形式证明的自动化的进展，如Mizar，Coq，Isabelle和HOL Light等证明助手。
2014-08-24 cs.LO math.LO
Logical Relations for Formally Verified Authenticated Data Structures
本文提出基于新型关系分离逻辑的形式化证明方法，为可自动生成认证数据结构的库验证安全性与正确性，证明了库优化的正确性及手写实现与自动生成代码的可靠链接，结果已在Coq中通过Iris框架机械化验证。
2025-01-18 cs.LO cs.PL
Computable analysis and notions of continuity in Coq
本文在 Coq 中基于 Incone 库形式化证明可计算分析中的多个定理，提供可执行算法并验证其正确性，同时比较不同连续性概念，贡献在于为连续结构上的算法推理提供通用接口。
2021-05-11 cs.LO
Single-set cubical categories and their formalisation with a proof assistant (extended version)
本文提出含连接与逆的立方 ω-范畴单集合公理化，通过范畴等价证明其合理性，并借助 Isabelle/HOL 完成形式化。
2024-07-04 cs.LO math.CT
Translating Scala Programs to Isabelle/HOL
我们提出了一个值得信赖的莱昂验证系统和伊莎贝尔证明助手之间的连接。Leon是一个用于验证Scala程序功能的系统。它使用各种自动定理证明器（ATP）来检查源于输入程序的验证条件（VC）。另一方面，Isabelle是一个交互式定理证明器，用于使用自己的输入语言Isabelle/Isar验证数学规范。用户指定（归纳）定义并手动编写关于它们的证明，尽管有半自动化策略的帮助。这两个系统的集成，使我们能够利用伊莎贝尔丰富的标准库，并给予更大的信心，保证分析程序的正确性。
2016-07-06 cs.LO
Foundations of Machine-Checked Control Theory in Lean
University of Melbourne（墨尔本大学）
该研究在精益中引入开源库用于机器验证控制理论，给出李雅普诺夫稳定性理论和小增益定理的形式化，前者用邻域滤波器涵盖多种系统，后者通过新方式证明，还介绍了库架构等及未来计划。
2026-07-23 cs.LO cs.SY eess.SY
Fully Mechanized Proofs of Dilworths Theorem and Mirskys Theorem
在Coq证明助手中给出了Dilworths定理和Mirskys定理的两个完全机械化的证明。Dilworths定理指出，在任何有限偏序集（偏序集）中，最小链覆盖和最大反链的大小是相同的。Mirskys定理是Dilworths定理的一个对偶。我们用Perles [2]（对Dilworths定理）和Mirsky [5]（对对偶定理）形式化了证明。我们还提出了一个图书馆的定义和事实，可以作为一个框架，形式化其他定理的有限偏序集。
2017-03-17 cs.DM cs.LO
An approach to translating Haskell programs to Agda and reasoning about them
我们使用Agda程序设计语言和证明助手来正式验证基于HotStuff / LibraBFT的拜占庭容错共识实现的正确性。Agda实现是我们基于LibraBFT的Haskell实现的翻译。这篇简短的论文集中在这项工作的一个方面。我们开发了一个库，使翻译后的Agda实现能够紧密地反映它所基于的Haskell代码。这使得更容易和更有效地审查翻译的准确性，并在Haskell代码更改时维护翻译的Agda代码，从而降低翻译错误的风险。我们还解释了我们如何捕捉我们的库提供的语法功能的语义，从而使正式的推理程序使用它们，我们如何推理所产生的Agda实现的细节将在未来的论文。我们提供的库独立于我们的特定验证项目，并且是开源的，可供其他人使用和扩展。
2022-05-18 cs.LO cs.PL cs.SE
Hipster: Integrating Theory Exploration in a Proof Assistant
本文介绍了一个集理论探索与证明助手Isabelle/HOL于一体的系统Hipster。理论探索是一种在给定的理论发展中自动发现新的有趣引理的技术。Hipster可以在两种主要模式下使用。第一种是探索模式，用于在新的理论发展中自动生成关于给定数据集和函数的基本引理。第二种是证明模式，用于特定的证明尝试，试图发现缺失的引理，以证明当前的目标。Hipster的证明模式补充并提升了现有的证明自动化技术，这些技术依赖于自动选择现有的引理，通过发明需要归纳来证明的新引理。我们展示了这两种模式的示例使用。
2014-05-14 cs.LO cs.MS
Small Scale Reflection for the Working Lean User
本文介绍了 Lean 4 证明助手中的 Small Scale Reflection（LeanSSR）方法与策略语言，利用原生元编程在内部实现，无需显式切换表示即可无缝结合演绎与计算证明，案例显示其能显著减小证明规模。
2024-03-19 cs.LO cs.PL
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
我们提出了简单的新的霍尔逻辑和精化演算的混合系统的风格的微分动态逻辑。（细化）Kleene代数与测试用于推理程序结构和生成验证条件在这一级。透镜以通用代数方式捕获混合程序存储。该方法已正式与伊莎贝尔/霍尔证明助手。一些示例解释了工作流程和最终的验证组件。
2019-10-29 cs.LO
Abduction Prover in Isabelle/HOL
Institute of Computer Science, the Czech Academy of Sciences（捷克科学院计算机科学研究所）
针对基于表达逻辑的证明助手自动化程度低的问题，提出了一种利用溯因推理识别有用猜想并自动构建证明脚本的Isabelle/HOL溯因证明器。
2026-06-03 cs.AI cs.LO cs.PL
On Exams with the Isabelle Proof Assistant
Technical University of Denmark（丹麦技术大学）
我们提出了一种方法来测试学生的学习成果，在自动推理的过程中使用伊莎贝尔证明助手。该方法使我们能够测试一般理解的形式证明在各种逻辑证明系统和理解的证明，特别是在高阶逻辑的伊莎贝尔/HOL。使用Isabelle几乎可以自动对考试的大部分内容进行评分。我们通过一些示例问题来解释我们的方法，并解释为什么我们认为我们选择的每种问题都足以衡量我们预期的学习成果。最后，我们讨论了我们的经验，使用的方法考试的课程自动推理，并建议潜在的未来工作。
2023-03-10 cs.AI cs.LO
Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology
Otto-Friedrich-Universität Bamberg（奥托-弗里德里希-班贝格大学）；Freie Universität Berlin（柏林自由大学）；University of Luxembourg（卢森堡大学）
本文介绍基于LogiKEy方法，利用经典高阶逻辑和证明助手Isabelle/HOL教授多元逻辑，通过系列谜题展示从命题到道义逻辑的教学路径，并反驳单一主义质疑，强调其可移植性。
2026-10-07 cs.AI cs.LO
BARReL: a modern backend for Atelier B in Lean
Université de Lorraine（洛林大学）；CNRS（法国国家科学研究中心）；Inria（法国国家数字与工程研究所）；LORIA
BARReL 是一个 Lean 4 库，桥接工业 B 方法工具 Atelier B 与 Lean 证明助手，支持在 Lean 中交互式进行 B 开发，通过显式良定义条件编码部分算子，并利用依赖类型保证良定义性，同时提供基本自动化。
2026-10-21 cs.LO
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
我们已经正式Szemerédi的正则引理和罗斯定理的算术级数，两个主要结果在极值图论和加法组合，使用证明助手伊莎贝尔/HOL。对于后者的形式化，我们使用前者首先显示三角形计数引理和三角形删除引理：本身重要的技术成果。在这里，除了展示主要的形式化陈述和定义之外，我们还关注证明中的敏感点，描述我们如何克服遇到的困难。
2022-10-13 cs.LO
Mechanization of Separation in Generic Extensions
我们机械化，在证明助手伊莎贝尔，证明公理计划的分离通用扩展模型的集合论使用的基本定理的强制。我们还形式化了可拓性、基础、联合和幂集公理的满足。无限公理同样处理，在额外的假设下的地面模型。为了实现这些目标，我们扩展了保尔森的图书馆的可构造性与内部化的公式变量的重命名，改善了结果的定义递归的基础良好的关系，并尖锐的假设，在他的发展相对化和绝对化。
2019-01-10 cs.LO math.LO
AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics
Axiomatic AI；Institut de Ciències Fotòniques (ICFO)（光子科学研究所）；Massachusetts Institute of Technology (MIT)（麻省理工学院）；Institució Catalana de Recerca i Estudis Avançats (ICREA)（加泰罗尼亚研究与高级研究所）
该研究发布了AxQM，这是物理学领域规模最大的教科书级证明综合基准，含1019个任务，用于评估自动形式化系统，所有任务保证有解且由Lean内核确定性评分。
2026-09-07 cs.AI cs.LO quant-ph
Infinite Words and Morphic Languages Formalized in Isabelle/HOL
我们提出了一个形式化的基本知识，无限的话，在通用的证明助手伊莎贝尔/HOL。此外，我们提出了一个形式化的纯形态和形态语言。最后，我们提出了一个形式化的定义Sturmian词作为低机械词，并证明了一些非常基本的事实。形式化是基于一个正在进行的更大的项目的形式化组合的话。
2023-03-20 cs.FL cs.LO
jsCoq: Towards Hybrid Theorem Proving Interfaces
MINES ParisTech PSL Research University（巴黎高等矿业学院PSL研究大学）
我们描述了jsCcoq，一个新的平台和用户环境的Coq交互式证明助手。jsCoq系统以HTML5-ECMAScript 2015规范为目标，它通常在符合标准的浏览器中运行，不需要外部服务器或服务。针对教育用途，jsCoq允许用户立即开始与证明脚本进行交互，这要归功于其自包含的性质。事实上，一个完整的Coq环境与证明脚本一起打包，简化了分发和安装。开始使用jsCoq就像点击一个链接一样简单。当前版本提供了10多个流行的Coq库，并支持流行的书籍，如Software Foundations或Certified Programming with Dependent Type。新的目标平台开辟了新的互动和展示可能性。它还促进了一些新的辅酶相关技术的发展。特别是，我们已经实现了一个新的基于序列化的协议，用于与证明助手进行交互，以及一个新的包格式用于库分发。
2017-01-25 cs.HC cs.LG cs.LO
Certifying Differential Equation Solutions from Computer Algebra Systems in Isabelle/HOL
Isabelle/HOL证明助手具有强大的库，可用于连续分析，为混合系统的验证提供了基础。然而，Isabelle缺乏对连续工件的自动化证明支持，这意味着验证通常是手动的。相比之下，计算机代数系统（CAS），如Mathematica和SageMath，包含大量用于矩阵、微分方程和其他相关工件的有效算法。然而，这些算法没有被验证，因此它们的输出本身不能被信任用于安全关键系统。在本文中，我们将两个CAS系统集成到Isabelle中，目的是证明常微分方程的符号解。这支持了一种自动化和可信的验证技术。
2021-02-04 cs.LO math.DS
Machine-Learned Premise Selection for Lean
University of Warsaw（华沙大学）；Czech Technical University（捷克技术大学）；University of Edinburgh（爱丁堡大学）；Carnegie Mellon University（卡内基梅隆大学）
本研究为Lean证明助手开发了基于在线训练定制随机森林的机器学习前提选择工具，直接依托Lean 4元编程特性实现，用mathlib数据训练，支持编辑器交互式调用，兼顾集成度、易用性与轻量高效性。
2023-06-14 cs.AI cs.LG cs.LO
ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
University of Texas, Austin, USA（得克萨斯大学奥斯汀分校）
提出ProofWala框架，通过itp-interface库实现与交互式定理证明器的程序化交互，支持多语言证明数据合成、并行证明搜索，并验证了跨语言与跨领域迁移的有效性。
2026-05-29 cs.AI cs.LG cs.LO
I/O Logic in HOL --- First Steps
University of Luxembourg（卢森堡大学）
提出了输入输出逻辑在经典高阶逻辑中的语义嵌入。这种嵌入使机械化和自动化的推理任务的输入/输出逻辑与现成的高阶定理证明和证明助手。这里提出的解决方案的关键思想来自对先前不准确的嵌入尝试的分析，我们也将讨论。
2018-04-19 cs.AI cs.LO
Initial Semantics for higher-order typed syntax in Coq
初始语义学旨在将与签名相关联的语法表征为某个类别的初始对象。我们提出了一个初步的语义结果类型的高阶语法连同其形式化的Coq证明助手。主要定理在2010年第二作者的博士论文中首次在纸上证明，并在不久后正式验证。对于固定的对象类型集合T上的简单类型绑定签名S，我们将一个称为S的表示范畴的范畴联系起来。我们证明了这个范畴有一个初始对象Sigma（S）。从它的构造中可以清楚地看出，对象Sigma（S）值得与S相关联的名称抽象语法。通过大量使用依赖类型，我们的定理在证明助手Coq中实现并证明了正确性。通过单子的方法产生了一种语法实现，其中术语和变量都是固有类型的，即对象类型反映在元级别类型中。这篇文章被看作是一篇研究文章，而不是关于一个经典数学结果的形式化。我们的定理的性质-涉及冗长，技术证明和复杂的代数结构-使它特别有趣的形式化验证。我们的目标是促进使用计算机定理证明器作为研究工具，并因此，一种新的方式出版的数学成果：一个平行的描述定理及其形式化应允许验证正确转录的定义和声明到证明助手，和简单，但技术证明应该很好地隐藏在一个数字图书馆。我们认为，科克的丰富的类型论，结合其各种功能，如隐式参数，允许一个特别可读的形式化，因此非常适合数学交流。
2011-09-17 cs.LO math.LO
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
我们研究各种配方的完整性一阶逻辑措辞建设性类型论和机械化的Coq证明助手。具体而言，我们研究的经典和直觉主义的自然演绎和微积分的变种模型论，代数和博弈论语义的完整性。作为完整性方面的标准模型理论语义的塔斯基和Kripke是不容易建设性的，我们分析连接的完整性定理，马尔可夫原理和弱柯尼希引理，并讨论非标准的语义承认无故障的完整性。我们贡献了一个可重用的Coq库一阶逻辑包含本文所涉及的所有结果。
2021-12-14 cs.LO math.LO
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
我们给出了我们在证明助手Isabelle/HOL中的形式化的概述，这些证明助手来自三篇不同的研究论文：Erdenses和Straus（1974），Hančl（2002），Hančl和Rucki（2005）。我们在Isabelle/HOL中的形式化可以在形式证明档案中找到。在这里，我们描述了选定的方面的形式化，并讨论这揭示了伊莎贝尔/HOL在形式化现代数学研究的使用和潜力，特别是在这些部分的数论和分析。
2021-04-26 cs.LO math.LO
Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL
University of Luxembourg（卢森堡大学）；Freie Universität Berlin（柏林自由大学）
给出了Carmo和Jones提出的并元道义逻辑在经典高阶逻辑中的一个浅语义嵌入。这种嵌入被证明是健全和完整的，也就是说，忠实。这里提出的工作提供了理论基础，并在现成的高阶定理证明和证明助手的二元道义逻辑的实施和自动化。
2018-03-05 cs.AI cs.LO math.LO
Smart Induction for Isabelle/HOL (System Description)
Czech Technical University in Prague（布拉格捷克理工大学）；University of Innsbruck（因斯布鲁克大学）
证明助手提供策略来促进归纳证明。然而，它仍然需要人类的聪明才智来决定什么论点传递给那些归纳策略。为了自动化这个过程，我们提出了Isabelle/HOL的smart_induct。给定任何问题域中的归纳问题，smart_induct会列出归纳策略的有希望的参数，而无需依赖于搜索。我们的评估表明，smart_induct在问题域中产生了有价值的建议。
2020-01-27 cs.AI cs.LO cs.PL
130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?
AI4REASON；University of Gothenburg（哥德堡大学）
该项目通过简单且低成本的方法，在两周内用LLM和证明检查器实现了大量拓扑学形式化，展示了自动形式化的可行性。
2026-01-06 cs.AI cs.LO cs.SC
