The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
Czech Technical University（捷克理工大学）；Radboud University（拉德堡德大学）
我们提出战术家，一个战术学习者和证明的Coq证明助手。Tactician帮助用户做出战术证明决策，同时保留对一般证明策略的控制。为此，Tactician从以前编写的战术脚本中学习，并为用户提供关于下一个要执行的战术的建议，或者完全接管证明合成的责任。Tactician的目标是为用户提供无缝、交互和直观的体验，以及强大和自适应的证明自动化。在本文中，我们从用户的角度对Tactician进行了概述，包括日常使用和在大范围学习时的包依赖管理问题。最后，我们将介绍Tactician作为Coq插件和机器学习平台的实现。
2020-07-31 cs.AI cs.LO
Performing Implicit Induction Reasoning with Certifying Proof Environments
传统的基于显式归纳模式的归纳方法在模式层次上是非约简的、局部的，被证明助手广泛采用。另一方面，自动定理证明器使用的隐式归纳方法允许懒惰和相互归纳推理。本文提出了一种新的策略，使Coq证明助手能够自动进行隐式归纳推理。通过使用一个自动的黑盒方法，拟由集成了Coq的认证证明环境手动证明的命题由Spike隐式归纳定理证明器证明。最终的证明随后被翻译成经过认证的Coq脚本。
2013-07-31 cs.LO
Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
Key Laboratory of High Confidence Software Technologies (Peking University), Ministry of Education（高可信软件技术教育部重点实验室）；School of Computer Science, Peking University, Beijing, China（北京大学计算机学院）
本文提出Strat2Rocq方法，通过提取LLM的证明策略来增强符号证明器的能力，提升自动化证明效果。
2026-03-04 cs.LO
Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
Preferred Networks, Inc.（首选网络公司）
自动定理证明（ATP）中的问题求解可以被解释为证明者逐步构造证明树的搜索问题。本文提出了一种用于直觉命题逻辑中证明搜索的深度强化学习算法。将深度学习应用于ATP的最大挑战是缺乏大型公共定理数据库。然而，我们通过在强化学习的每次迭代中应用新的数据增强过程来克服这个问题。我们还提高了算法的效率，通过一种新的紧凑图表示公式的语法结构。使用大量的扩充数据，我们训练高度精确的图神经网络，其近似公式的语法结构的集合的价值函数。我们的方法在计算时间方面也具有成本效益。我们将展示我们的证明器优于Coq的$\texttt{tauto}$策略，这是一种基于人类工程学的证明器。在指定的时间限制内，我们的证明器解决了基准库中84%的定理，而$\texttt{tauto}$只能解决52%。
2018-11-02 cs.AI cs.LG cs.LO
MirrorShard: Proof by Computational Reflection with Verified Hints
我们描述了一种在Coq证明助手中构建可组合且可扩展的验证过程的方法。与依赖于运行时生成和检查证明的传统方法不同，我们使用经过验证的正确过程与Coq可靠性证明。虽然他们是内在的Coq的逻辑，我们的证明支持声音扩展用户提示新的领域，使自动推理用户定义的抽象谓词。我们通过开发一个用于模块化包装，构建和组成提示数据库的体系结构来保持稳健性，该体系结构以前仅在其动态类型化，证明生成策略语言的级别上在Coq中实现。我们的证明器还包括对统一变量的丰富处理，使其能够与Coq中其他基于策略的演绎步骤集成。我们已经实现了我们的技术，在反射验证的开源框架，XNUMX碎片。我们证明了它的适用性，通过实例化它的分离逻辑，以理由有关的强制性程序验证。
2013-05-28 cs.LO cs.PL
A Normalizing Intuitionistic Set Theory with Inaccessible Sets
我们提出了一个集理论强大到足以解释强大的类型论的基础证明助手，如乐高，也可能Coq，这在同一时间，使程序提取其建设性的证明。为了这个目的，我们公理化Zermelo-Fraenkel集理论IZF与替换和$ω$ -许多不可接近的，我们称之为\izfio的一个不可预测的建设性版本。我们的公理化利用集条款，一个归纳的定义不可访问的集合和相互递归性质的平等和成员关系。它允许我们根据Curry-Howard同构原则定义一个弱规范化类型λ演算，对应于\izfio中的证明。我们使用可实现性来证明规范化定理，这为程序抽取能力提供了基础。
2008-04-08 cs.LO
PIDE for Asynchronous Interaction with Coq
本文介绍了初步的进展，对集成的Coq证明助手与PIDE架构最初开发的伊莎贝尔。该架构旨在与证明助手进行异步、并行交互，并且与允许jEdit编辑器与Isabelle一起工作的插件紧密相关。我们对PIDE架构进行了一些概括，以适应更多的证明器，而不仅仅是Isabelle，并调整Coq以理解核心协议：这在大约两个人工月内交付了一个工作系统。
2014-10-30 cs.HC cs.LO
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
本文为直觉主义强Löb逻辑提出新相继式演算，实现强终止的向后搜索与句法消割，并在Coq中形式化验证。
2023-09-01 cs.LO math.LO
On the (Intuitionistic) Logic of Next-Token Prediction
University of North Texas（北德克萨斯大学）
该研究在直觉主义蕴含逻辑中建模生成式AI的下一个令牌预测，推导等价于乘法RNN的神经架构，用Prolog定理证明器验证模型性质，并将其与Transformer等模型对比。
2026-08-11 cs.LO
Proof Automation in the Theory of Finite Sets and Finite Set Relation Algebra
{log}（'setlog'）是有限集理论和有限集关系代数（FSTRA）公式的可满足性求解器。因此，它可以用作该理论的自动定理证明器（ATP）。{log}能够自动证明一些FSTRA定理，但不是所有的。然而，我们已经观察到，{log}不能自动证明的许多定理可以被分成几个子目标，这些子目标可以由{log}自动排出。这项工作的目的是提出一个原型交互式定理证明器（ITP），称为{log}-ITP，提供证据表明，一个适当的集成到世界一流的ITP的{log}可以提供大量的证明自动化有关FSTRA。基于TPTP和Coq的SSReflect库中的210个定理的经验评估显示，Coq证明的大小和复杂性明显减少。
2021-01-19 cs.LO
Verified completeness in Henkin-style for intuitionistic propositional logic
本文在Lean定理证明器中形式化并验证了Troelstra和van Dalen提出的直觉主义命题逻辑Henkin式完备性证明，是该方法下首个经机械验证的同类成果，源码已开源。
2023-10-03 cs.LO
A Machine Checked Model of Idempotent MGU Axioms For Lists of Equational Constraints
我们提出了形式化的证明，验证了一阶统一算法定义的可满足的约束列表生成一个最一般的统一（MGU），这也恰好是幂等的。我们所有的证明都在Coq定理证明器中得到了形式化。我们的证明表明，由统一算法产生的有限映射提供了一个模型的公理表征幂等MGU的约束列表。作为我们验证的基础的公理是从一个标准集通过将它们扩展到约束列表而得出的。对我们来说，约束是简单类型语言中术语之间的等式。使用Coq库Coq.FSets.FMapInterface将替换正式建模为有限映射。Coq的函数归纳法是证明许多公理的主要证明技术。
2010-12-22 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
Recycling Proof Patterns in Coq: Case Studies
University of Dundee（邓迪大学）
交互式定理证明器的发展导致了大型图书馆和各种形式证明基础设施的创建。然而，尽管（或者可能是由于）它们的复杂性，非专家或跨领域的库的重用是一个挑战。在本文中，我们提供了详细的案例研究和评估机器学习工具ML4PG建立交互式数据挖掘的电子图书馆的证明，并提供用户指导的基础上，证明模式在现有的图书馆。
2014-03-07 cs.AI cs.LG cs.LO
Implementing the First-Order Logic of Here and There
University of Pernambuco（巴伊亚大学）；University of Potsdam（波茨坦大学）
本文提出了一种基于sequent 计算机和直觉逻辑嵌入的HT一阶逻辑自动定理证明器，并通过基准测试验证了其有效性。
2026-01-07 cs.AI cs.LO cs.PL
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
本文提出Lean-auto，一种在Lean 4与自动定理证明器之间的翻译算法，首次在Lean 4中实现基于ATP的通用证明自动化，保证健全性并在Mathlib4上优于现有工具。
2025-05-24 cs.LO
An Automatically Verified Prototype of the Android Permissions System
在以前的工作德卢卡和卢娜提出了正式规范的理想化配方的权限模型的Android在Coq证明助手。这个正式的开发大约是23 Kbps的Coq代码，包括证明。这项工作的目的是表明，{log}（“setlog”）-一个可满足性求解器和约束逻辑程序设计语言-可以被用来作为一个有效的自动证明类的证明，必须履行的形式化验证的系统，如一个进行了德卢卡和卢娜。我们展示了Coq模型是如何在{log}中编码的，以及如何执行自动化证明。生成的{log}模型是Android权限系统的自动验证的可执行原型。在执行{log}中的所有证明后，提供了有关经验评估的详细数据。Coq和{log}的集成，以提供一个具有自动化证明和原型生成的框架进行了讨论。
2022-09-21 cs.LO cs.SE
Automated verification of termination certificates
为了增加用户的信心，许多自动定理证明器提供可以独立验证的证书。在本文中，我们报告了我们的进展，在开发一个独立的工具，用于检查证书的正确性终止长期重写系统，并正式证明其正确性的证明助手Coq。为此，我们使用Coq的提取机制和库上的重写理论和终止称为CoLoR。
2012-12-11 cs.LO cs.MS cs.SE
Introduction to Pylog
本文介绍极简实验性证明助手 PyLog，它以线性化自然演绎支持带概括算子的直觉主义和经典一阶逻辑，并通过 Curry-Howard 对应与 Coq 等依赖类型论工具形成互补。
2023-06-05 cs.LO math.LO
Sharing a Library between Proof Assistants: Reaching out to the HOL Family
我们今天观察到大量的证明系统的多样性。这种多样性的负面后果是，许多定理被证明了许多次。与程序设计语言不同，这些系统很难协同工作，因为它们不实现相同的逻辑。逻辑框架是一类定理证明器，它们通过实现各种逻辑的能力来克服这个问题。在这项工作中，我们研究了STTforall逻辑，简单类型论，已被编码在逻辑框架Dedukti的扩展。我们提出了一个翻译从这个逻辑OpenTheory，证明系统和互操作性工具之间的证明HOL家庭。我们已经使用这个翻译导出了一个包含费马小定理的算术库到OpenTheory和另外两个证明系统Coq和Matita。
2018-07-05 cs.LO
SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
为解决一阶自动定理证明器到交互式定理证明器的证明迁移问题，提出 TPTP 推导格式扩展 SC-TPTP，支持序列形式体系，并实现工具库以解析、检查证明并导出至 Coq。
2025-07-15 cs.LO
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
我们研究各种配方的完整性一阶逻辑措辞建设性类型论和机械化的Coq证明助手。具体而言，我们研究的经典和直觉主义的自然演绎和微积分的变种模型论，代数和博弈论语义的完整性。作为完整性方面的标准模型理论语义的塔斯基和Kripke是不容易建设性的，我们分析连接的完整性定理，马尔可夫原理和弱柯尼希引理，并讨论非标准的语义承认无故障的完整性。我们贡献了一个可重用的Coq库一阶逻辑包含本文所涉及的所有结果。
2021-12-14 cs.LO math.LO
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
我们提出了一个综合的两个证明风格的交互式定理证明：程序风格（其中证明是脚本的命令，如在Coq）和声明式风格（其中证明是文本在一个受控的自然语言，如在Isabelle/Isar）。我们的方法结合了声明式风格的优点-编写正式证明的可能性，如正常的数学文本-和程序风格-强大的自动化和帮助形成的证明，包括确定中间步骤的声明。我们的方法是新的，显着不同的方式，程序和声明式的证明风格已经结合在伊莎贝尔，Ssreflect和Matita系统。我们的方法是通用的，可以实现任何程序的交互式定理证明器，无论其架构和逻辑基础。为了展示我们提出的方法的可行性，我们将其完全实现为一个名为miz 3的证明接口，位于HOL Light交互式定理证明器之上。这个接口使用的声明式语言是Mizar系统语言的一个轻微变体，可以用于任何交互式定理证明器，无论其逻辑基础如何。miz 3界面允许轻松访问HOL Light的全套战术和正式库，因此具有“工业实力”。我们的方法提供了一种方法，自动转换任何程序的证明，一个声明的副本，其中转换后的证明是类似的大小，原来的。由于所有的声明式系统本质上都有相同的证明语言，这提供了一种在交互式定理证明器之间移植证明的简单方法。
2012-03-27 cs.LO
Formalized Lambek Calculus in Higher Order Logic (HOL4)
在这个项目中，一个相当完整的证明理论形式化的Lambek演算（非关联的任意扩展）已经从Coq证明辅助移植到HOL4定理证明器，并进行了一些改进和新的定理。定义了Lambek演算的三个演绎系统（句法演算、自然演绎和序列演算），并证明了许多相关定理。形式上证明了这些系统之间的等价性。最后，在HOL4中设计并实现了序列微积分证明的形式化（其中Coq具有内置支持）。一些基本结果，包括所谓的“割自由”证明的子公式的性质进行了形式证明。这项工作可以被认为是对语言解析器的基础上的类别语法，这是不是多模态的，但仍然有能力支持上下文敏感的语言，通过自定义的扩展的初步工作。
2017-05-20 cs.CL cs.LO
Characteristics of de Bruijn's early proof checker Automath
本文聚焦de Bruijn早期证明检查器Automath的句法背景与不常见方面，提出一个封装最常见版本的通用Automath系统，并以现代句法框架呈现，该系统基于CC的扩展λD。
2022-06-15 cs.LO math.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
GamePad: A Learning Environment for Theorem Proving
University of California, Berkeley（加利福尼亚大学伯克利分校）；OpenAI（开放人工智能研究中心）
在本文中，我们介绍了一个名为GamePad的系统，可以用来探索应用机器学习方法的定理证明在Coq证明助手。交互式定理证明器（如Coq）使用户能够以逐步的方式构建机器可检查的证明。因此，他们提供了一个机会，探索定理证明与人类的监督。我们使用GamePad来合成一个简单的代数重写问题的证明，并训练Feit-Thompson定理的形式化的基线模型。我们处理位置评估（即，预测剩下的证明步骤的数量）和策略预测（即，预测下一个证明步骤）任务，这些任务在基于策略的定理证明中自然出现。
2018-12-21 cs.AI cs.LG cs.LO
Towards Automated Readable Proofs of Ruler and Compass Constructions
Faculty of Mathematics, University of Belgrade（贝尔格莱德大学数学学院）
本文提出让三角形作图求解器 ArgoTriCS 结合一阶逻辑与相干逻辑自动定理证明器，为尺规作图生成人类可读且可由 Coq、Isabelle/HOL 检查的形式化正确性证明。
2024-01-22 cs.AI cs.LO
Formalization, Mechanization and Automation of Gödel's Proof of God's Existence
Freie Universität Berlin（柏林自由大学）；Vienna University of Technology（维也纳技术大学）
哥德尔的本体论证明已经分析了第一次与前所未有的详细程度和形式的帮助下，高阶定理证明。以下是已经完成的（并按此顺序）：一个详细的自然演绎证明。TPTP THF语法中公理、定义和定理的形式化。使用Nitpick自动验证公理和定义的一致性。自动证明定理与证明LEO-II和Satallax。使用Coq证明助手的逐步形式化。使用Isabelle证明助手的形式化，其中定理（和一些额外的引理）已使用Sledgehammer和Metis自动化。
2017-09-03 cs.AI cs.LO math.LO
Mechanized Undecidability of Higher-order beta-Matching (Extended Version)
TU Dortmund University（多特蒙德工业大学）
本文通过字符串重写系统证明了高阶β匹配的不可判定性，并利用Coq验证了该结果。
2026-08-12 cs.LO
Proof Automation with Large Language Models
Purdue University（普渡大学）
针对LLM在Coq等交互式定理证明器中生成正式证明时低层细节易错的问题，提出PALM生成后修复方法，利用符号方法迭代修复LLM生成的初始证明，显著提升了定理证明数量并超越现有方法。
2024-09-22 cs.AI cs.LG cs.LO
