Level-Confluence of 3-CTRSs in Isabelle/HOL
我们提出了一个伊莎贝尔/HOL形式化的早期结果由铃木，Middeldorp和伊达，即某一类条件重写系统是水平融合。我们的形式化基本上是沿着原始证明的路线，我们主要在细节水平以及关于一些基本定义方面偏离原始证明。
2016-02-23 cs.LO
Isabelle/HOL as a Meta-Language for Teaching Logic
证明助手是逻辑教学的重要工具。我们支持这一主张，讨论三个形式化的Isabelle/HOL在最近的课程中使用的自动推理。第一个是系统W（一个只有两个原始符号的经典命题逻辑系统）的形式化，第二个是自然演绎助手（NaDeA），第三个是使用我们的序列演算验证器（SeCaV）的单边递归演算。我们依次描述每个形式化，集中在我们如何在教学中使用它们，并从逻辑教育的角度评论有趣或有用的功能。最后，我们反思了所吸取的经验教训，以及这些经验教训下一步可能引导我们走向何方。
2020-10-30 cs.LO
A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
在Isabelle/HOL中形式化量子信息基本概念，证明局域隐变量假设不成立，并形式化CHSH不等式违反相关结果及Tsirelson界。
2023-06-21 cs.LO quant-ph
Formalization of Complex Vectors in Higher-Order Logic
复向量分析在物理学和工程学等许多学科中被广泛用于分析连续系统。在本文中，我们提出了一个高阶逻辑形式化的复向量空间，以方便进行这种分析的声音的核心定理证明：HOL光。我们对复向量的定义建立在复数和实向量的定义之上。这种扩展使我们能够广泛地受益于已经验证的定理的基础上复杂的分析和真正的向量分析。为了显示我们的图书馆的实用性，我们采用它来形式化电磁场，并证明了平面波的反射定律。
2014-05-15 cs.LO
A Formalization of Martingales in Isabelle/HOL
本文在Isabelle/HOL中形式化了任意巴拿赫空间上的鞅理论，将条件期望从实数推广到巴拿赫空间，定义了随机过程及鞅类，并证明了平均定理以确立密度的唯一性。
2023-11-10 cs.LO math.PR
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
Matching concepts across HOL libraries
许多证明助手库包含相同数学概念的形式化。这些概念通常以不同的方式引入（定义），但它们所具有的属性以及相应的形式化是相同的。对于基本概念，比如自然数，由于数学命名约定，在库之间匹配它们通常很简单。然而，对于更高级的概念，即使对于专家来说，在不同的库中找到类似的形式化也是一项重要的任务。在本文中，我们研究了自动发现的相似概念，跨图书馆的证明助手。我们提出了一种规范化的正式图书馆和一些相似性措施的概念属性的方法。我们在基于HOL的证明助手HOL 4、HOL Light和Isabelle/HOL上对该方法进行了评估，发现了398对同构常数和类型。
2014-05-15 cs.LO
On the Formalization of Network Topology Matrices in HOL
School of Electrical Engineering and Computer Science（电气与计算机工程学院）；Concordia University, Montreal, QC, Canada（康考迪亚大学）；National University of Sciences and Technology, Islamabad, Pakistan（国立科学与技术大学）
本文利用HOL交互式定理证明形式化网络拓扑矩阵，验证其性质并分析电路中的Kron缩减和总功率耗散。
2026-03-26 cs.LO math.AT
Gröbner Bases of Modules and Faugère's $F_4$ Algorithm in Isabelle/HOL
我们提出了一个优雅的，通用的和广泛的形式化的格罗布纳基在Isabelle/HOL。形式化涵盖了理论的所有要点（多项式约简、S-多项式、Buchberger算法、Buchberger避免无用对的准则），但也包括更高级的特征，如约简的格罗布纳基。特别突出的是第一次形式化的福格尔的矩阵为基础的$F_4$算法和事实，即整个理论制定的模块和子模块，而不是环和理想。所有形式化的算法都可以被转换成在具体数据结构上运行的可执行代码，从而实现（简化的）格罗布纳基和合冲模块的认证计算。
2018-05-01 cs.LO cs.SC
Formalization of Differential Privacy in Isabelle/HOL
本文提出一个通用的 Isabelle/HOL 差分隐私形式化库，首次支持连续概率分布，并验证了标准定义、Laplace 机制和 report noisy max 机制。
2024-10-20 cs.CR cs.LO cs.PL
L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
本文在Isabelle/HOL中完整形式化了L-mosaics与有界并半格等价性的对象部分，采用AI辅助方法验证了主要理论结果及变换互逆性，展示了多值代数运算深度与AI增强定理证明的潜力。
2025-09-24 cs.LO math.AC
Formal Probabilistic Analysis of Dynamic Fault Trees in HOL4
动态故障树（DFT）是一种广泛使用的故障建模技术，可以以非常有效的方式捕获系统的动态故障特征。模拟和模型检验传统上用于DFT的概率分析。仿真通常基于采样，因此不能保证其结果是完整的，而模型检验使用计算机算术和数值算法来计算概率的精确值，其中包含许多舍入误差。利用高阶逻辑（HOL）定理证明的表达和声音的性质，我们提出了，在这项工作中，DFT门和它们的概率行为，以及它们的一些简化性质的形式化HOL。这种形式化将允许我们通过验证关于其在HOL中的行为的通用数学表达式来进行DFT的概率分析。特别是，我们形式化的AND，OR，优先级AND，功能DEPPER，热SPARE，冷SPARE和暖SPARE门，并验证其相应的概率表达式在HOL。此外，我们正式验证了一个重要的属性，Pr（X<Y），使用Lebesgue积分，因为这种关系允许我们推理优先级-“与”门和Before运算符的概率属性。我们还正式的概念，条件密度，以正式验证的概率表达式的冷SPare和暖SPare门。为了说明我们的形式化的有用性，我们用它来正式分析心脏辅助系统的DFT。
2018-07-24 cs.LO
Formalization of Bond Graph using Higher-order-logic Theorem Proving
键合图是描述复杂工程和物理系统动力学的统一图形方法，广泛应用于电气、机械、医学、热力学和流体力学等领域。传统上，这些动态分析使用纸和笔的证明方法和基于计算机的技术。然而，这两种技术都有其固有的局限性，如人为错误倾向，结果的近似和巨大的计算需求。因此，这些技术不能被信任用于执行基于键合图的动态分析系统的安全关键领域，如机器人和医学。形式化方法，特别是高阶逻辑定理证明，可以克服这些传统方法的缺点，并提供这些系统的准确分析。它已被广泛应用于工程和物理系统的动力学分析。在本文中，我们提出使用高阶逻辑定理证明进行键合图的物理系统的分析。特别是，我们提供了键合图的形式化，其中主要包括功能，允许键合图转换到其相应的数学模型（状态空间模型）和验证其各种属性，如，稳定性。为了说明我们所提出的方法的实际有效性，我们提出了正式的稳定性分析的假肢机电一体化的手使用HOL光定理证明。此外，为了帮助HOL中的非专家，我们在MATLAB中编码我们正式验证的稳定性定理，以执行拟人假肢机电一体化手的稳定性分析。
2021-11-24 cs.LO
A Formalization of Unique Solutions of Equations in Process Algebra
在这篇论文中，一个全面的形式化米尔纳的演算通信系统（也称为CCS）已经完成了在HOL定理证明器（HOL 4），在HOL 88的旧工作的基础上。这包括强/弱互模拟等价和观测同余的所有经典性质，CCS的同余理论，各种版本的“互模拟高达”技术，以及几个深层定理，即“弱等价中包含的粗同余”，以及Milner书中的三个版本的“方程的唯一解”定理。这项工作进一步扩展到支持并发理论的最新发展，即“收缩”关系和相关的“收缩的唯一解”定理由博洛尼亚大学的Davide Sangiorgi教授发现。因此，本文还形式化了一个相当完整的CCS“收缩”（以及一个类似的关系称为“膨胀”）理论。在此基础上，作者发现了一种新的收缩变形，称为“观测收缩”。形式上证明了这种新的关系是CCS过程的直和所保持的，并且具有一种更优美的形式的“压缩唯一解”定理，而不受CCS文法的任何限制.
2017-12-05 cs.LO cs.PL
Quantum projective measurements and the CHSH inequality in Isabelle/HOL
我们提出了一个形式化的Isabelle/HOL的量子投影测量，一类测量涉及正交投影仪，经常用于量子计算。我们还形式化了CHSH不等式，这一结果在任意概率空间都成立，可以用来反驳量子力学中局部隐变量理论的存在性。
2021-03-15 cs.LO
Complex Bounded Operators in Isabelle/HOL
RWTH Aachen（亚琛工业大学）；University of Tartu（塔尔图大学）；Université Laval（拉瓦尔大学）
本文在Isabelle/HOL中形式化了复向量空间上的有界算子，包括复范数空间、巴拿赫空间、希尔伯特空间，定义了有界算子类型cblinfun，并发展了酉算子、投影算子、有界线性函数延拓定理、伴随算子、Loewner序、闭子空间等理论，同时为有限维情况提供了与矩阵的代码生成支持。
2026-05-31 cs.LO
Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL
该研究在 Isabelle/HOL 中完成了 STARK 风格透明证明协议的形式化，构建了含证明者/验证者可执行模型等内容的开发成果，为相关领域提供了形式化方法层面的支撑。
2026-09-23 cs.LO cs.SE
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 Biological Circuit Block Diagrams for formally analyzing Biomedical Control Systems in pHRI Applications
本文提出在pHRI场景下用HOL Light定理证明器对生物医学控制系统框图进行形式化建模与演绎推理，并以超滤透析控制为例验证方法有效性。
2024-12-31 cs.LO
Conversion of HOL Light proofs into Metamath
我们提出了一个算法转换证明从OpenTheory交换格式，它可以被翻译成和从任何的HOL家庭的证明语言（HOL4，HOL光，ProofPower，和伊莎贝尔），到ZFC为基础的Metamath语言。该任务分为两个步骤：将OpenTheory证明转换为Metamath HOL形式化$\mathtt{\text{hol.mm}}$，然后将HOL形式化嵌入到主Metamath库$\mathtt{\text{set.mm}}$的主要ZFC基础中。这个过程提供了一种方法，将Metamath基础的简单性与在HOL Light中取得成果的强烈自动化努力联系起来，允许在HOL Light中产生完整的Metamath定理证明，同时也证明HOL Light相对于Metamath的ZFC公理化是一致的。
2015-06-18 cs.LO math.LO
Formalization and Implementation of Algebraic Methods in Geometry
我们描述了我们正在进行的项目的代数方法的形式化几何定理证明（吴的方法和Groebner基地的方法），其实施和整合的教育工具。该项目包括对Isabelle/HOL证明助手中的代数方法进行形式化验证，并开发一个新的、开源的代数方法Java实现。该项目应填补这一领域仍然存在的一些空白（例如，代数方法和综合几何之间缺乏正式的联系，以及缺乏适合于与动态几何工具集成的代数方法的独立实现），并且应该能够在教育中实现定理证明的新应用。
2012-02-22 cs.LO cs.MS cs.SC
Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs
由于Avenhaus和Loría-Sáenz，我们提出了一个Isabelle/HOL形式化的准还原强确定性条件项重写系统的汇流特性。
2016-09-12 cs.LO
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
本文基于证明助手Isabelle/HOL，利用自由逻辑的浅层语义嵌入对范畴论进行元逻辑研究，形式化了初等拓扑斯与对称幺半闭范畴，并构建了易于使用的Isabelle范畴论库，为未来形式化研究奠定基础。
2023-06-16 cs.LO math.CT math.LO
Formalized Lambek Calculus in Higher Order Logic (HOL4)
在这个项目中，一个相当完整的证明理论形式化的Lambek演算（非关联的任意扩展）已经从Coq证明辅助移植到HOL4定理证明器，并进行了一些改进和新的定理。定义了Lambek演算的三个演绎系统（句法演算、自然演绎和序列演算），并证明了许多相关定理。形式上证明了这些系统之间的等价性。最后，在HOL4中设计并实现了序列微积分证明的形式化（其中Coq具有内置支持）。一些基本结果，包括所谓的“割自由”证明的子公式的性质进行了形式证明。这项工作可以被认为是对语言解析器的基础上的类别语法，这是不是多模态的，但仍然有能力支持上下文敏感的语言，通过自定义的扩展的初步工作。
2017-05-20 cs.CL cs.LO
Formal Analysis of Continuous-time Systems using Fourier Transform
为了研究工程和物理系统的动力学行为，我们经常需要捕捉它们的连续行为，这是使用微分方程建模，并执行这些系统的频域分析。传统上，使用基于纸笔的分析技术或计算机模拟，使用傅立叶变换方法来执行该频域分析。然而，这两种方法都容易出错，因此不适用于分析安全关键领域（如医学和运输）中使用的系统。为了提供一个准确的替代方案，我们建议使用高阶逻辑定理证明进行频域分析这些系统。为此，本文提出了一个高阶逻辑形式化的傅立叶变换使用HOL-Light定理证明。特别地，我们使用基于高阶逻辑的多变量微积分的微分、积分、超越和拓扑理论的形式化来形式化地定义傅立叶变换，并推理其经典性质的正确性，例如存在性、线性、时移、频移、调制、时间标度、时间反转和时域微分，以及其与傅立叶余弦的关系，傅立叶正弦和拉普拉斯变换。我们使用我们提出的形式化的形式化验证的频率响应的一般n阶线性系统，音频均衡器和MEMS加速度计，使用霍尔光定理证明。
2017-07-31 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
Munkres' General Topology Autoformalized in Isabelle/HOL
Independent（独立研究者）；Aalborg University（奥尔堡大学）；University of Melbourne（墨尔本大学）；AI4REASON and University of Gothenburg / Chalmers University（AI4REASON 和哥德堡大学 / 查尔姆斯理工大学）
本研究利用LLM辅助在Isabelle/HOL中自动形式化Munkres泛拓扑教材，生成85000余行代码，涵盖39章节，证明包括Tychonoff定理等核心结果，方法结合声明性证明与sledgehammer工具，展现高效形式化潜力。
2026-04-08 cs.AI cs.LG cs.LO
Dynamic Dependability Analysis of Shuffle-exchange Networks using HOL Theorem Proving
为了克服传统可靠性模型建模的局限性，引入了动态可靠性模型，如动态故障树（DFTs）和动态可靠性框图（DRBDs）。最近，高阶逻辑（HOL）形式化的两个模型已经进行，这使得这些模型的分析正式，在一个定理证明。在这份报告中，我们提供了正式的动态可靠性分析洗牌交换网络，这是多级互连网络，通常用于多处理器系统。我们使用DFT和DRBDs模型的终端，广播和网络的可靠性与动态备用门，并在几个通用版本的结构。我们验证这些系统的故障概率和可靠性的通用表达式，它可以被实例化与任何数量的系统组件和故障率的原因，这些网络的故障行为。
2019-10-24 cs.LO
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
Microsoft（微软）；Centro de Informática, Universidade Federal de Pernambuco（巴西联邦伯南布哥大学信息学中心）
本文在Lean 4中形式化了任意维数的斯托克斯定理，通过弗雷歇导数实现真正微分形式拉回，并结合mathlib4的extDeriv抽象，扩展了链级斯托克斯理论，验证了奇异立方链的d²=0性质。
2026-05-01 cs.LO math.DG
Towards the Certification of Complexity Proofs
我们报告我们的形式化的矩阵解释在伊莎贝尔/HOL。矩阵需要证明终止证明，我们希望利用它们的复杂性证明，太。对于后者的目标，只有基本的方法已经被整合，我们讨论了一些即将出现的问题时，形式化更复杂的结果矩阵的解释，这是基于凯莱-汉密尔顿定理或联合谱半径理论。
2012-08-08 cs.LO
A Linter for Isabelle: Implementation and Evaluation
在交互式定理证明中，形式化质量是开发的可维护性和可重用性的关键因素，也会影响证明检查性能。通常，导致质量问题的反模式对于有经验的用户来说是已知的。然而，在许多定理证明器系统中，没有自动工具来检查它们的存在并使经验不足的用户意识到它们。我们试图通过开发一个linter作为一个公共可用的附加组件来填补Isabelle环境中的这一空白。linter提供了基本的可配置性、可扩展性、Isabelle/jEdit集成和独立的命令行工具。我们在Isabelle/HOL中发现了480个潜在问题，在Isabelle分布的其他形式化中发现了14016个问题，在AFP中发现了惊人的59573个问题。对于AFP提交的特定lint捆绑包，我们发现在1595个案例中违反了提交指南。我们着手缓解Isabelle/HOL中的问题，到目前为止解决了168个问题;我们发现，大多数情况下，高严重性的lint与实际问题相对应，个人用户经常在许多地方犯同样的错误，并且回顾性地解决这些问题需要大量的工作。相比之下，为新开发交互式地解决这些问题通常只会带来很少的开销，正如我们在一个有22名参与者的定量用户调查中发现的那样（超过60%的参与者不到一分钟）。我们还发现，对问题的良好解释是用户容易解决这些问题（相关系数0.48）和他们对最终结果满意度（相关系数0.62）的关键。
2022-07-21 cs.LO
Polymorphism Meets DHOL
University of Innsbruck（因斯布鲁克大学）；University of Melbourne（墨尔本大学）；University of Erlangen-Nuremberg（埃尔朗根-纽伦堡大学）
本文提出多态性DHOL，通过扩展HOL实现依赖类型，提升高阶逻辑在数据结构、范畴论等领域的应用效率，并通过工具实现自动化证明。
2026-07-01 cs.LO
Towards the Formal Performance Analysis of Multistate Coherent Systems using HOL Theorem Proving
许多实际工程系统及其组件具有多个性能水平和故障模式。如果这些系统相对于其组件的性能形成单调增加的结构函数（系统模型），并且如果它们的所有组件影响整个系统的性能，则它们被称为多态相干系统。传统上，这些多态相干系统的可靠性分析已经进行了使用纸和笔或基于仿真的方法。前一种方法通常容易出现人为错误，而后者对于具有多个操作状态的组件的大型复杂系统需要高计算资源。作为一种补充方法，本文提出使用高阶逻辑（HOL）定理证明来建立一个合理的推理框架来分析多态相干系统的可靠性。该框架使我们能够正式验证具有任意数量的分量及其状态的多态相干系统的一般数学性质。特别地，我们提出了串联和并联多态相干系统的HOL形式化，并使用HOL4定理证明器正式验证其确定性和概率性质。为了说明的目的，我们提出了正式的可靠性分析的多州石油和天然气管道，以证明我们提出的框架的有效性。
2021-12-24 cs.LO
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
本文针对依赖类型高阶逻辑DHOL提出原生表推演自动推理规则，并在Lash中实现，借助DHOL到HOL的可靠完备翻译保证完备性，实验表明其性能优于在翻译结果上运行的主流HOL证明器。
2024-10-18 cs.LO
A Formally Verified HOL4 Algebra for Event Trees
事件树（ET）分析作为一种前向演绎安全分析技术，在关键系统设计阶段被广泛用于决策。ET是表示系统中所有可能的操作状态和外部事件的示意图，以便这些可能的场景之一可能发生。在这份报告中，我们建议使用HOL 4定理证明的形式化建模和步骤分析的ET图。为此，我们在高阶逻辑中开发了一种基于通用列表数据类型的ET图的形式化，该数据类型可以：（i）构建任意级别的ET图;（ii）减少不相关的ET分支;（iii）划分ET路径;以及（iv）基于某些事件的发生进行概率分析。为了说明的目的，我们进行正式的ET逐步分析的电网，并确定其系统平均中断频率指数（SAIFI），这是一个重要的指标，系统的可靠性。
2020-04-29 cs.LO cs.SY eess.SY
A formal proof of modal completeness for provability logic
本研究在HOL Light定理证明器中实现哥德尔-勒布可证性逻辑（GL）模态完备性的形式化证明，介绍实现细节与非标准证明结构选择，并分析该形式化系统推理的优缺点。
2021-02-11 cs.LO math.LO
Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms
本文扩展了PVS环理论，形式化了Euclidean域的唯一析因性并验证了整数环等结构，同时规范了Euclidean gcd算法并证明其正确性可继承至具体结构。
2024-04-23 cs.LO
Towards Formal Fault Tree Analysis using Theorem Proving
National University of Sciences and Technology (NUST)（国立科技大学）
故障树分析（FTA）是一种可靠性分析技术，已被广泛用于预测许多复杂工程系统的可靠性、可用性和安全性。传统上，这些基于FTA的分析是使用纸笔证明方法或计算机模拟完成的，由于其固有的局限性，这些方法不能确定绝对正确性。作为一种补充方法，我们建议使用高阶逻辑定理证明器HOL 4进行基于FTA的安全关键系统的故障分析的准确性是一个迫切需要的分析。特别是，本文提出了一个高阶逻辑形式化的通用故障树门，即，与、或、与非、或非、异或和非的失效概率表达式的形式化验证。此外，我们已经正式验证了通用的概率包含-排除原则，这是进行任何给定系统的基于FTA的故障分析的最重要的要求之一。为了说明的目的，我们进行基于FTA的故障分析的太阳能电池阵，这是用来作为东方红3号（DFH-3）卫星的主要电源。
2015-05-08 cs.AI cs.LO cs.SE
