Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
在同一问题的形式化上比较证明者总是一个有价值的练习。在本文中，我们提出了一个非平凡的算法的正确性的形式证明，从图论中进行了三个证明助手：Why3，Coq和Isabelle。
2018-10-29 cs.LO
Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant
我们提出的证明丢番图'第20个问题（第六册丢番图'算术），其中包括想知道是否存在直角三角形的双方可以衡量为整数和其表面可能是一个广场。这个问题在17世纪被费马否定地解决了，他使用了无限下降的“奇妙”方法（ipse difficult Fermat）。这种方法，在历史上是归纳法的第一次使用，包括产生越来越小的非负整数解，假设存在一个;这自然会导致反证推理，因为我们以零为界。我们描述了这种证明的形式化已进行的Coq证明助手。此外，作为一个直接的和同样具有历史意义的应用，我们还提供了费马最后定理（n=4）的证明（由费马），以及Coq中相应的形式化。
2005-10-04 cs.LO cs.SE math.NT
Computing in Coq with Infinite Algebraic Data Structures
编码到构造性类型论证明中的计算内容可用于在具体数据结构上进行计算实验。在本文中，我们探讨这种可能性时，在Coq与链复合物的无限型（也就是说，产生的无限集）作为一个层次的同调代数结构的形式化的一部分。
2010-04-28 cs.LO
Formalization of Quantum Protocols using Coq
量子信息处理是物理学和计算机科学交叉的一个令人兴奋的研究领域，具有影响信息处理系统未来发展的巨大潜力。实用的、通用的量子计算机的建造可能要到未来几年。然而，量子通信和量子密码学已经发展得很好。商业量子密钥分发系统很容易获得，世界各地已经内置的了几个QKD网络。在这些实现中使用的协议的安全性依赖于信息理论证明，这可能会或可能不会反映实际的系统行为。此外，对实现的测试不能保证没有bug和错误。本文提出了一种新的量子协议建模和验证框架，并使用证明助手Coq实现。我们为量子比特（qubit）、量子门和量子测量提供了一个Coq库。作为验证实际量子通信和安全协议（如量子密钥分发）的一步，我们支持多量子比特，通信和纠缠。我们通过对量子隐形传态协议进行建模来说明这些概念，该协议仅使用经典信道来传达未知量子比特的状态。
2015-11-05 cs.CR cs.LO
A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory
该研究在Coq证明助手中以接口形式形式化单子效应层级与代数定律，分离定律与模型，结合Coq重写能力与引理库实现简洁程序证明，还可用于单子模型形式化及含引用ML子集的等式定律设计。
2023-12-11 cs.LO
A preliminary univalent formalization of the p-adic numbers
在本文中，我们给出了一个初步的形式化的p-adic数，在第二作者的单叶基金会计划的背景下。在证明辅助工具Coq中给出了相应的验证代码。由于在单价设置的工作正在进行中，我们在本文中给出的p-adic数的结构和组织的建设预计将改变Coq库更合适的重新排列，并优化，由作者和其他研究人员在未来。因此，我们这里的构造应被视为第一近似，有待改进。
2013-02-05 cs.LO math.LO
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
本文全面介绍了在 Coq 中形式化 Lebesgue 微分定理的工作，并由此得到 Lebesgue 积分的第一微积分基本定理，同时大幅丰富了 MathComp-Analysis 库并给出 Urysohn 引理的新证明。
2024-06-30 cs.LO
Formalizing May's Theorem
这份报告提出了一个形式化的梅定理的证明助手Coq。它描述了定理陈述是如何首先被翻译成Coq定义的，以及它是如何被证明的。文中讨论了证明和相关工作的各个方面。据作者所知，这个项目是第一个记录的尝试机械化梅定理。
2022-10-11 cs.LO
A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
本文在 Coq 中形式化兼具概率选择与非确定性选择的几何凸单子，提炼凸空间等可复用理论，构建支持效应等式推理的框架。
2020-10-26 cs.LO
Formalized linear algebra over Elementary Divisor Rings in Coq
本文给出了初等除子环上线性代数的Coq形式化，初等除子环是指每个矩阵都等价于一个Smith范式矩阵的环。主要结果是这些环支持线性代数的本质运算的形式化，这类环上的非表示模的分类定理以及Smith范式直到单位乘的唯一性.我们提出了正式验证算法计算这种范式的各种系数结构，包括欧几里德域和建设性的主要理想域。我们还研究了不同的方法来扩展Bézout域，以便能够计算史密斯范式的矩阵。我们考虑的扩展是：充分性（即存在一个gdco操作），Krull维数$\leq 1$和良好的严格整除。
2016-06-20 cs.LO math.RA
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
A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories
在本文中，我们提出了一个形式化的Kozen的命题模态$μ$ -演算，在演算的归纳结构。我们解决了几个有问题的问题，如使用高阶抽象语法在归纳集合中存在的递归构造器，编码的模态（“证明”）规则和上下文敏感的语法。该编码可用于\Coq系统中，为$μ$ -演算中的无错证明的交互式开发提供了一个实验性的计算机辅助证明环境。我们采用的技术可以很容易地移植到其他语言和证明系统具有类似的问题。
1998-09-29 cs.LO
Formalization of the Axiom of Choice and its Equivalent Theorems
本文描述了Morse-Kelley集合论中选择公理的形式化及其几个著名的等价定理。这些定理包括Tukey引理、Hausdorff极大值原理、极大值原理、Zermelo公设、Zorn引理和良序定理。我们依次用选择公理证明上述定理，最后用Zermelo公设和良序定理证明选择公理，从而完成了它们之间等价性的循环证明。使用Coq证明助手对证明进行了形式化的检查，其中Morse-Kelley集理论被形式化。整个形式证明过程表明，基于Coq的数学定理机器证明具有高度的可靠性和严密性。本文的形式化工作对于大多数应用，特别是在集合论、拓扑学和代数学中的应用是足够的。
2019-06-10 cs.FL cs.LO
Lebesgue Induction and Tonelli's Theorem in Coq
勒贝格积分是一种著名的数学工具，例如用于概率论、实分析和数值数学。因此，它在证明助手中的形式化被设计成适合不同的目标和项目。一旦勒贝格积分的正式定义和第一引理证明，方便的问题的形式化自然出现。为了检验它，一个有用的扩展是托内利定理，指出一个非负的两个变量的可测函数的（二重）积分可以通过迭代积分计算，并允许切换积分的顺序。因此，我们需要定义和证明乘积空间上的结果，希望它们可以很容易地从单个空间上的现有结果导出。本文描述了乘积$σ$ -代数的形式定义和证明，乘积测度及其唯一性，迭代积分的构造，直到Tonelli定理。我们还为{ \nonnegative }可测函数宣传归纳类型提供的\emph{Lebesgue induction principle}。
2022-02-10 cs.LO math.FA
Machine Learning of Coq Proof Guidance: First Experiments
University of Innsbruck（因斯布鲁克大学）
我们报告的第一个实验的结果与学习证明依赖与Coq系统完成的形式化。我们解释了从Coq证明中获得依赖关系的过程，用于学习的公式的特征，以及评估方法。各种机器学习方法进行了比较的5021 toplevelCoq证明来自CoRN存储库的数据集。最好的结果方法覆盖了前100个预测中平均75%的所需证明依赖关系，这与其他大型理论语料库上的初始实验相当。
2014-10-20 cs.LG cs.LO
CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
University of Pittsburgh（匹兹堡大学）；IBM Research（IBM研究院）；IHES（高等科学研究所）
强化学习算法通过优化长期奖励来解决概率环境中的顺序决策问题。在安全关键设置中使用强化学习的愿望激发了最近的正式约束强化学习的工作;然而，这些方法将学习算法的实现放在其可信计算基础上。这些实现的关键正确性属性是学习算法收敛到最优策略的保证。本文通过开发两个规范的强化学习算法：有限状态马尔可夫决策过程的值和策略迭代的Coq形式化，开始了缩小这一差距的工作。中心的结果是贝尔曼的最优性原理及其证明的形式化，它使用了贝尔曼最优性算子的收缩性质来建立一个序列收敛于无限视界极限。CertRL的开发说明了Giry monad和机械化度量共归纳如何简化强化学习算法的最优性证明。CertRL库提供了一个通用框架，用于证明马尔可夫决策过程和强化学习算法的属性，为进一步开展强化学习算法的形式化工作铺平了道路。
2020-12-15 cs.AI cs.LO cs.PL
Mechanizing Matching Logic In Coq
匹配逻辑是使用模式和模式匹配来指定和推理数学结构的形式体系。它越来越流行，已被用来定义许多逻辑系统，如具有递归定义的分离逻辑和线性时态逻辑。此外，它还作为K语义框架的逻辑基础，该框架用于为许多现实世界的语言构建实用的验证器。尽管匹配逻辑是一个容纳大量理论的基本形式系统，但它缺乏通用的、机器检查的形式化。因此，我们使用Coq证明助手来形式化匹配逻辑。具体来说，我们创建了一个新的表示匹配逻辑，使用本地无名编码，我们正式的语法，语义和证明系统，这种表示在Coq证明助手。最重要的是，我们证明了形式化证明系统的可靠性，并提供了一种在Coq中进行交互式匹配逻辑推理的方法。我们相信这项工作提供了一个以前未探索的途径推理匹配逻辑，其模型和证明系统。
2022-09-21 cs.LO
Context-Free Language Theory Formalization
证明助手是基于软件的工具，用于数学和计算机科学中证明构造和验证的机械化，也用于认证程序开发。为了加速和简化证据核查，正在越来越多地使用各种工具。上下文无关语言理论是一个成熟的数学领域，与计算机科学基础和技术相关。该提案旨在形式化Coq证明助手中的部分上下文无关语言理论。本报告介绍了证明助手的基本理论和一般特征，包括Coq本身，讨论了它在相关形式化项目中的使用，介绍了目前的实施情况，讨论了相关项目和这项工作的贡献。到目前为止，所获得的结果包括形式化的封闭属性的上下文无关文法（union，concatenation和closure）和形式化的语法简化。语法简化是计算机语言处理技术和形式语言理论中的一个重要课题，形式化是指一般的上下文无关文法生成的语言也可以由更简单等价的上下文无关文法生成。在保留原文法生成的语言方面，描述了无用符号消除、不可达符号消除、单位规则消除和空规则消除操作，并证明了这些操作的正确性。
2015-05-01 cs.FL cs.LO
A Formalized Extension of the Substitution Lemma in Coq
本文在 Coq 中形式化验证了扩展显式替换算子后的 lambda 演算语法下替换引理仍然成立，采用 nominal 方法处理 alpha 等价，为不同显式替换演算提供了通用框架。
2023-09-25 cs.LO
Formalized Lambek Calculus in Higher Order Logic (HOL4)
在这个项目中，一个相当完整的证明理论形式化的Lambek演算（非关联的任意扩展）已经从Coq证明辅助移植到HOL4定理证明器，并进行了一些改进和新的定理。定义了Lambek演算的三个演绎系统（句法演算、自然演绎和序列演算），并证明了许多相关定理。形式上证明了这些系统之间的等价性。最后，在HOL4中设计并实现了序列微积分证明的形式化（其中Coq具有内置支持）。一些基本结果，包括所谓的“割自由”证明的子公式的性质进行了形式证明。这项工作可以被认为是对语言解析器的基础上的类别语法，这是不是多模态的，但仍然有能力支持上下文敏感的语言，通过自定义的扩展的初步工作。
2017-05-20 cs.CL cs.LO
Measure Construction by Extension in Dependent Type Theory with Application to Integration
本文在 Coq 中利用 Mathematical Components 与 Hierarchy-Builder，通过集合半环上的测度延拓形式化 Lebesgue 测度，为兼容的 Lebesgue 积分奠定基础。
2023-06-06 cs.LO
Martin-Löf à la Coq
我们在Coq证明助手中提出了Martin-Löf类型论（MLTT）的元理论的广泛机械化。我们的开发建立在Agda中已有的工作的基础上，不仅展示了转换的可判定性，而且还展示了类型检查的可判定性，使用双向类型检查指导的方法。从我们的可判定性证明，我们获得了一个认证和可执行的类型检查器的一个成熟的版本的MLTT与$Π$，$Σ$，$\mathbb{N}$，和身份类型的支持，和一个宇宙。此外，我们的发展不依赖于不可预测性，归纳递归或任何超越MLTT的公理，具有索引归纳类型和少数谓词宇宙的模式，将对象理论和元理论之间的差距缩小到仅仅是宇宙的差异。最后，我们解释了我们的形式化选择，面向模块化的发展依赖于Coq的功能，例如元编程设施提供的战术和宇宙多态性。
2023-10-10 cs.LO cs.PL
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
A formalization of convex polyhedra based on the simplex method
在证明助手Coq中给出了凸多面体的形式化。我们的工作的基石是一个完整的实施单纯形法，连同证明其正确性和终止。这允许我们以有效的方式定义多面体上的基本谓词（即，作为程序），并将它们与相应的通常的逻辑对应物相关联。为此，我们广泛使用布尔反射方法。这种方法的好处是，我们可以很容易地推导出多面体上的几个基本结果的证明，如Farkas引理，线性规划的对偶定理和Minkowski定理。
2018-08-10 cs.LO math.CO math.OC
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
本文描述了离散实闭域在Coq证明助手中的形式化。这个抽象的结构捕捉例如实代数数的理论，一个具有良好算法性质的实数的可判定子集。实代数数和更一般的半代数簇的理论是实分析中许多有效方法的核心，包括非线性算术的决策过程或实值函数的优化方法。在定义了离散实闭域的抽象结构和多项式实根的基本理论之后，根据计算机代数中关于量词消去的标准文献，给出了一个基于伪余项序列的代数证明的形式化.这种形式化涵盖了理论的很大一部分，这是在计算机代数实践中实现的有效算法的基础。这项工作的成功为这些有效方法的正式认证铺平了道路。
2012-02-15 cs.LO
Certified Impossibility Results for Byzantine-Tolerant Mobile Robots
我们提出了一个框架，建立正式的发展，机器人网络使用COQ证明助手，状态和证明正式的各种属性。在本文中，我们专注于不可能性证明，因为利用COQ高阶微积分来推理算法作为抽象对象是很自然的。我们提出特别是正式证明两个不可能的结果forconvergence的不经意的移动机器人，如果分别超过一半和超过三分之一的机器人表现出拜占庭故障，从原来的定理Bouzid等人。由于我们的形式化，相应的COQ发展是相当紧凑的。据我们所知，这些是机器人网络的第一个认证（在正式证明的意义上）不可能性结果。
2013-06-18 cs.DC cs.LO
A Coq Library of Sets for Teaching Denotational Semantics
本文提出一个基于 Coq 类型类系统的集合与关系库，用标准数学记号改善指称语义教学中的可读性，同时保持零证明项开销。
2024-04-08 cs.LO cs.PL
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq
集束蕴涵逻辑（BI）是构成分离逻辑主干的子结构逻辑，分离逻辑是研究堆操作程序推理的逻辑。虽然BI的证明理论和元理论在数学上都有涉及，但重要的元理论结果的形式化仍然刚刚起步。在本文中，我们提出了一个自包含的形式化，在Coq的证明助手，证明了中央元理论性质的BI：削减消除其微积分。提出的证明是 * 语义 *，在这个意义上说，是通过解释在一个特定的“通用”模型的序列。这导致了一个比标准的Gentzen风格的切割消除参数更模块化和优雅的证明，这在BI的手动证明中可能是微妙和容易出错的。特别是，我们的语义方法避免了不必要的反演证明推导，或使用削减减少和多削减规则。除了模块化，我们的方法也是强大的：我们演示了我们的方法规模，与微小的修改，（i）BI的扩展与任意一组的\emph{simple structural rules}，和（ii）扩展与S4一样的$\Box$模态。
2021-12-10 cs.LO math.LO
Existentially Quantified Systems of Equations as an Implicit Representation of Answers in Logic Programming
在本文中，我们提出了另一种方法来形式化的逻辑编程理论。在这种形式化中，我们允许在查询中存在量化变量和方程。与标准方法相反，答案的作用将由存在量化的方程组发挥。这使得我们在处理替换时可以避免问题。特别地，当输入子句引入新变量时，我们不需要“全局”变量分隔条件。此外，这种形式化可以被视为并发逻辑语言理论的基础，因为它还包括广泛的并行计算方法。此外，答案的平行组合可以直接定义为答案的一致连接。
2022-07-19 cs.LO cs.PL
Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic
我们开发了一个线性逻辑框架内的混合系统，并使用它来推理的类型系统的量子λ演算。特别是，我们认为一个实用的版本的演算称为原Quipper，其中包含的核心Quipper。Quipper是一种正在积极开发的新量子程序设计语言，最近在量子计算社区中获得了很大的普及。Hybrid是一个系统，旨在支持使用高阶抽象语法（HOAS）来表示和推理Coq证明助手中实现的正式系统。在这项工作中，我们扩展了系统的线性规格说明逻辑（SL），以理由Quipper的线性型系统。为此，我们形式化的原型Quipper的语义编码的SL中的类型和评价规则，并证明类型的可靠性。
2018-12-10 cs.LO cs.PL
Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version)
Xavier Leroy和Sandrine Blazy在2007年使用Coq证明助手对低级命令式语言（如C）的内存模型进行了形式化验证。考虑到他们的形式化基本上是在一阶逻辑中进行的，作者留下的一个问题是，他们的证明是否可以使用一阶逻辑的验证框架自动化。我们接受了挑战，并使用Why3自动化了它们的形式化，大大减少了证明工作。我们系统地遵循Coq证明，并意识到在许多情况下，Why3能够释放所有VC的方式大约是三分之一。此外，仍然需要交互的证明（例如归纳，存在性证明的证人，断言）被分解为我们明确声明的辅助结果。通过这种方式，我们实现了记忆模型的几乎自动的可靠性和安全性证明。尽管如此，我们的发展允许提取一个正确的构造具体的记忆模型，因此比Leroy和Blazy的初步版本更进一步。
2022-12-05 cs.LO cs.PL
Towards a constructive formalization of Perfect Graph Theorems
图的团数$ω(G) $和色数$χ(G) $之间的相互作用是图论中一个很好的研究课题。完美图定理可能是这方面最重要的结果。图$G$称为\emph{perfect}，如果对$G$的每个导出子图$H$都有$χ(H)=ω(H)$。强完美图定理（SPGT）指出一个图是完美的当且仅当它不包含奇洞（或奇反洞）作为它的导出子图。弱完美图定理（WPGT）指出，一个图是完美的，当且仅当它的补图是完美的。在本文中，我们提出了一个正式的框架来验证这些结果。我们在Coq证明助手的构造性类型论中对有限简单图进行建模，并在此框架下给出了弱完美图定理证明的核心思想Lovász复制引理的构造性证明.
2018-12-28 cs.DM cs.LO
Formalization of some central theorems in combinatorics of finite sets
我们提出了充分形式化的证明，从组合学的一些中心定理。这些是Dilworth的分解定理，Mirsky的定理，霍尔的婚姻定理和Erdens-Szekeres定理。Dilworth分解定理是其中的关键结果。它指出，在任何有限偏序集（偏序集）中，最小链覆盖和最大反链的大小是相同的。Mirsky定理是Dilworth分解定理的对偶，Dilworth分解定理指出在任何有限偏序集中，最小反链覆盖和最大链的大小相同。我们利用Dilworth定理证明了Hall婚姻定理和Erdens-Szekeres定理。这些定理所涉及的组合对象是集合和序列。所有的证明都在Coq证明助手中形式化。我们开发了一个图书馆的定义和事实，可以作为一个框架，形式化的其他定理有限偏序集。
2017-03-31 cs.DM cs.LO
Spreads and Packings of PG(3,2), Formally!
研究了如何在Coq证明助手中形式化最小射影空间PG（3，2）。然后，我们正式描述的蔓延和包装PG（3，2），以及他们的一些性质。形式化是相当简单的，然而，随着所涉及的对象数量的迅速增加，我们需要利用一些对称性参数以及智能证明技术来使证明搜索和验证更快，从而使用Coq证明助手更容易处理。这项工作可以被看作是形式化更高维的射影空间的第一步，例如PG（4，2），或更高阶的射影空间，例如PG（3，3）。
2022-01-03 cs.LO cs.SC
Extracting efficient exact real number computation from proofs in constructive type theory
本文提出在依赖类型论中对实数进行新公理化，使构造性证明可提取为基于 AERN 的高效精确实数计算程序，并在 Coq 中实现验证。
2022-02-02 cs.LO
Efficient Certified Resolution Proof Checking
我们提出了一种新的命题证明跟踪格式，消除了复杂的处理，从而实现有效的（正式）证明检查。这种格式的好处是通过在C中实现证明检查器来证明的，它比最先进的检查器性能高出两个数量级。然后，我们形式化的理论背后的命题证明检查Coq，并提取一个正确的构造证明检查我们的格式从形式化。使用来自2015年和2016年SAT竞赛的280个不可满足的实例进行的经验评估表明，该认证检查器通常执行最先进的非认证证明检查器。使用这种格式，我们正式验证了布尔毕达哥拉斯三重猜想的最近200 TB证明。
2016-10-29 cs.LO
A Constructive Formalization of the Weak Perfect Graph Theorem
完美图定理是描述图$G$的团数$ω(G) $与色数$χ(G) $之间关系的重要图论结果。一个图$G$称为\emph{perfect}，如果对于$G$的每个导出子图$H$都有$χ(H)=ω(H)$.强完美图定理（SPGT）指出一个图是完美的当且仅当它不包含奇洞（或奇反洞）作为它的导出子图。弱完美图定理（WPGT）指出，一个图是完美的，当且仅当它的补图是完美的。在本文中，我们提出了一个正式的框架，工作与有限的简单图。我们在Coq证明助手中建模有限简单图，将其顶点表示为可数无限域上的有限集。我们认为，这种方法提供了一个正式的框架，它是方便的工作与不同类型的图的构造（或扩展）涉及的证明的Lovász复制引理（LRL），这也是关键的结果，用于证明弱完美图定理。最后，我们使用这个设置开发一个建设性的形式化的弱完美图定理。
2019-12-04 cs.DM cs.LO cs.PL
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
Double Auctions: Formalization and Automated Checkers
本文将双向拍卖匹配算法扩展到多数量请求，在 Coq 中完成形式化与正确性证明，并抽取 OCaml/Haskell 程序用于自动检查交易所算法违规。
2024-10-24 cs.LO q-fin.TR
Formalizing the Face Lattice of Polyhedra
本文在 Coq 中首次形式化了多面体的面，构建了相关库并设计自动表示机制，证明了面的格性质及 Balinski 定理。
2022-05-17 cs.LO math.CO math.OC
VEL: A Formally Verified Reasoner for OWL2 EL Profile
Kansas State University（堪萨斯州立大学）
针对OWL推理器可靠性不足的问题，研究者开发了经形式化验证的EL++推理器VEL，基于Coq证明助手实现算法提取并修正了原算法的完备性缺陷，为高风险场景下的推理正确性提供了保障。
2024-12-11 cs.AI cs.LO cs.PL
