Formalizing Graph Trail Properties in Isabelle/HOL
我们描述了一个数据集表达和证明的图形轨迹的属性，使用Isabelle/HOL。我们形式化的推理严格增加和减少的痕迹，使用权重的边缘，并证明下界的加权图中的痕迹的长度。我们这样做，通过扩展的图论库Isabelle/HOL与算法计算的长度最长的严格减少图线索从一个顶点为给定的重量分布，并证明任何减少的线索也是一个增加的。本预印本已被CICM 2020接受出版。
2021-03-05 cs.LO
Lemmanaid: Neuro-Symbolic Lemma Conjecturing
Department of Computer Science and Engineering University of California, San Diego, USA（计算机科学与工程系，加州大学圣地亚哥分校）；Department of Computer Science and Engineering Chalmers University of Technology & University of Gothenburg（计算机科学与工程系，查尔姆斯理工大学及哥德堡大学）
提出首个神经符号引理猜想工具LEMMANAID，通过类比数学理论生成引理，结合微调LLM与符号方法，在Isabelle测试集上优于纯神经和纯符号方法。
2026-06-02 cs.AI cs.LO
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
我们描述了SeCaV，一阶逻辑在Isabelle/HOL，和SeCaV Unshortener，一个在线工具，扩展到完整的SeCaV语法简洁的推导的一阶逻辑的微积分验证。我们利用Isabelle/HOL作为SeCaV推导的证明检查器。Isabelle/HOL的交互功能使我们的系统透明。例如，用户可以简单地点击一个边条件来查看它的确切定义。我们的形式化的可靠性和完整性证明完全适用于暴露给用户的微积分，而不仅仅是我们工具的一些模型。用户还可以在SeCaV Unshortener中编写他们的派生，它提供了更轻的语法，并扩展它们以供以后验证。我们在教学中使用了这两种工具。
2022-04-08 cs.LO
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
证明助手，如Isabelle/HOL，提供了一些工具来促进归纳定理证明。Isabelle专家知道如何有效地使用这些工具;然而，有一点工具支持将这些专家知识传递给更广泛的用户受众。为了解决这个问题，我们提出了我们的领域特定的语言，LiFtEr。LiFtEr允许有经验的Isabelle用户以独立于任何问题域的风格编码他们的归纳推理。LiFtEr的解释器机械地检查归纳工具的给定应用程序是否与逻辑匹配，从而自动化知识传递循环。
2020-05-24 cs.LO
Translating Scala Programs to Isabelle/HOL
我们提出了一个值得信赖的莱昂验证系统和伊莎贝尔证明助手之间的连接。Leon是一个用于验证Scala程序功能的系统。它使用各种自动定理证明器（ATP）来检查源于输入程序的验证条件（VC）。另一方面，Isabelle是一个交互式定理证明器，用于使用自己的输入语言Isabelle/Isar验证数学规范。用户指定（归纳）定义并手动编写关于它们的证明，尽管有半自动化策略的帮助。这两个系统的集成，使我们能够利用伊莎贝尔丰富的标准库，并给予更大的信心，保证分析程序的正确性。
2016-07-06 cs.LO
A Formalisation of a Special Case of the Union-Closed Conjecture in Isabelle/HOL
Royal Holloway, University of London（伦敦大学皇家霍洛威学院）；University of Cambridge（剑桥大学）
该研究在 Isabelle/HOL 中形式化了并闭猜想特例的 2021 年证明，通过概述证明并展示代码片段，展示了数学推理在形式语言中的清晰表达。
2026-09-21 cs.LO
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
我们提出了简单的新的霍尔逻辑和精化演算的混合系统的风格的微分动态逻辑。（细化）Kleene代数与测试用于推理程序结构和生成验证条件在这一级。透镜以通用代数方式捕获混合程序存储。该方法已正式与伊莎贝尔/霍尔证明助手。一些示例解释了工作流程和最终的验证组件。
2019-10-29 cs.LO
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL
我们提出了一个证明过程中的Isabelle/HOL的一元实多项式问题。我们的过程的核心数学是基于单变量柱形代数分解。我们遵循不可信证书的方法，将解决与验证分离：高效的外部工具执行昂贵的真实代数计算，产生在Isabelle逻辑中正式检查的证据。这使我们能够利用高度调整的计算机代数系统，如Mathematica来指导我们的过程，而不会影响其结果的正确性。我们目前的实验证明这种方法的有效性，在许多情况下产生的数量级的改进，比以前的方法。
2018-04-10 cs.LO
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
我们介绍了一种语言，PSL，旨在捕捉高层次的证明策略在伊莎贝尔/HOL。给定策略和证明义务，PSL的运行时系统生成并组合各种策略，以低内存使用探索大搜索空间。一旦成功，PSL会生成一个高效的证明脚本，它绕过了大部分的证明搜索。我们还提出了PSL的一元解释器表明，PSL的基本思想是转移到其他ITP。
2017-03-02 cs.LO
Linear Programming in Isabelle/HOL
本文在 Isabelle/HOL 中实现了一个线性规划求解器，基于单纯形算法形式化和弱对偶定理，可形式化证明其可靠性与终止性，并能生成外部求解器。
2024-03-28 cs.LO
Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL
许多事实具有对称的对应物，通常需要单独的形式证明，这取决于所涉及的对称性的性质。我们介绍了一种方法在Isabelle/HOL产生这样一个对称的事实列表数据类型和对称性引起的列表反转映射。该方法作为属性实现，其结果基于用户声明的对称规则。除了一般的规则，我们提供的规则，旨在应用于领域的组合词。
2022-05-09 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
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL
仿真和形式化验证是基于模型的高可靠性系统开发的重要补充技术。为了支持一致的结果，有必要为这两个活动提供统一的语义和自动化。在本文中，我们应用Isabelle/HOL中的交互树产生一个验证和仿真框架的状态丰富的过程语言。我们开发的核心理论和验证技术的交互树，使用它们给CSP和马戏团的语言的语义，并正式连接我们的新语义与故障分歧的语义模型。我们还展示了如何伊莎贝尔代码生成器可以用来生成验证可执行的模拟反应和并发程序。
2021-05-11 cs.LO
Type Inference for Isabelle2Cpp
本文针对 Isabelle2Cpp 框架在 Isabelle/HOL 规范类型信息缺失时无法自动生成 C++ 代码的问题，提出了一种类型系统，通过引入新的类型推断规则和统一算法对中间表示表达式进行类型推断与统一，从而生成更完整准确的 C++ 代码。
2024-04-28 cs.LO
From LCF to Isabelle/HOL
交互式定理证明器在过去的四十年里得到了巨大的发展，从原始的开始到今天的强大系统。在这里，我们专注于Isabelle/HOL及其独特的优势。它们包括自动证明搜索，从一阶定理证明世界借用技术，但也自动搜索反例。它们包括一个高度可读的结构化证明语言和一个独特的交互式开发环境，用于编辑现场证明文档。一切都建立在Robin Milner为Edinburgh LCF设想的基础上：一个证明内核，使用抽象类型来确保可靠性并消除存储证明的需要。与20世纪70年代的研究原型相比，Isabelle是一个实用和通用的工具。它被系统设计师，数学家和许多其他人使用。
2019-07-17 cs.LO
Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL
在复分析中，缠绕数测量路径（逆时针）围绕一个点缠绕的次数，而柯西指数可以近似路径的缠绕方式。我们在Isabelle定理证明器中正式确定了这种近似，并提供了一种通过Cauchy指数来评估缠绕数的策略。通过进一步结合这种近似与辐角原理，我们能够利用剩余序列来有效地计算多项式在某些区域（如矩形盒和半平面）内的复根的数量。
2019-08-05 cs.LO
Brownian Motion in Isabelle/HOL
为形式化验证机器人控制器中的随机混合系统，本文在Isabelle/HOL中机械化布朗运动、随机核与马尔可夫半群，并证明Kolmogorov-Chentsov定理以构造Hölder连续修正，为演绎验证奠定基础。
2024-10-13 cs.LO
Formalizing IMO Problems and Solutions in Isabelle/HOL
国际数学奥林匹克（IMO）可能是世界上最著名的智力竞赛，因此也是人工智能（AI）面临的最大挑战之一。最近制定的IMO Grand Challenge要求建立一个可以在比赛中赢得金牌的AI。我们提出了一些初步的步骤，可以帮助解决这一目标，通过创建一个公共的存储库的机械检查的解决方案的IMO问题的交互式定理证明器伊莎贝尔/HOL。这个知识库由塞尔维亚贝尔格莱德大学数学系的学生在“交互式定理证明导论“课程中积极维护。
2020-10-30 cs.LO
Reconstructing veriT Proofs in Isabelle/HOL
自动定理证明器现在通常用于交互式定理证明器中，以履行越来越多的证明义务。为了保持证明的可信度，必须在证明助手中验证自动找到的证明。我们在这里提出了一个重建过程中的证明助手Isabelle/HOL证明生成的可满足性模理论求解器veriT这是smt策略的一部分。我们详细描述了我们改进的重建方法的架构和我们在设计它时所面临的挑战。我们的实验表明，VeriT驱动的SMT策略经常被Sledgehammer建议为自动解决证明目标的最快方法。
2019-08-26 cs.LO
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
University of Iowa（爱荷华大学）；Stanford University（斯坦福大学）
提出 Apply2Isar 工具，自动将 Isabelle/HOL 的 apply 风格脚本转换为可读性更强的 Isar 声明式证明，并在大型基准测试中验证其有效性。
2026-05-30 cs.LO
Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
本文提出一种分析Metis成功证明以提取变量实例化的新工具，从而提升Sledgehammer的成功率与证明速度，并帮助用户理解目标与引理之间的推导关系。
2025-08-28 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/HOL as a Meta-Language for Teaching Logic
证明助手是逻辑教学的重要工具。我们支持这一主张，讨论三个形式化的Isabelle/HOL在最近的课程中使用的自动推理。第一个是系统W（一个只有两个原始符号的经典命题逻辑系统）的形式化，第二个是自然演绎助手（NaDeA），第三个是使用我们的序列演算验证器（SeCaV）的单边递归演算。我们依次描述每个形式化，集中在我们如何在教学中使用它们，并从逻辑教育的角度评论有趣或有用的功能。最后，我们反思了所吸取的经验教训，以及这些经验教训下一步可能引导我们走向何方。
2020-10-30 cs.LO
Isabelle technology for the Archive of Formal Proofs with application to MMT
本文概述了形式证明档案（AFP）背后的Isabelle技术。交互式开发和准交互式构建工作对逻辑（通常是Isabelle/HOL）、数学工具实现的Isabelle/ML和物理系统集成的Isabelle/Scala提出了显著的可扩展性要求--所有这些都集成在Isabelle/PIDE（Prover IDE）中。AFP的持续增长要求Isabelle的性能不断改进。这是一份关于Isabelle 2019（2019年6月）情况的报告，其中包括显着的附加组件，如证明器会话导出和无头PIDE，用于基于语义信息的自动更新。一个示例应用程序是Isabelle/MMT，它能够将所有Isabelle + AFP转换为OMDoc和RDF三元组，但将Isabelle技术重用于其他应用程序是直接的。
2019-06-11 cs.LO
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs
我们扩展了混合系统的语义验证框架与Isabelle/HOL证明助手的混合程序存储的代数模型，混合程序及其正确性规范的浅层表达模型，和特定领域的演绎和计算支持。新的存储模型产生干净的分离和变量的动态局部视图，例如离散/连续，可变/不可变，程序/逻辑，以及使用组合子，投影和框架操纵它们的增强方式。这导致了更多的本地推理规则，程序和策略，用于使用不变集进行推理，验证混合规范的解决方案或计算具有增强的证明自动化和可扩展性的导数。新的表达式模型提供了更用户友好的语法，更好的名称空间控制和连接框架与真实世界建模语言的接口。
2021-06-10 cs.LO
Formalizing Pick's Theorem in Isabelle/HOL
本研究受HOL Light中皮克定理形式化工作启发，在Isabelle/HOL中调整证明策略规避了多边形内部分割的核心证明难点，同时从基础层面扩充现有几何库，完成皮克定理的形式化并反思了策略优劣。
2024-05-03 cs.LO
Verifying Numerical Methods with Isabelle/HOL
University of Aalborg（奥尔堡大学）；University of York（约克大学）
本文提出基于ITrees的Isabelle/HOL框架，用于验证数值方法，通过形式化规范和自动证明方法，实现从形式化到可执行代码的端到端验证流程。
2026-09-23 cs.LO
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
计算机代数和数值分析中的许多问题都可以归结为计算或近似计算一个区间内多项式的实根。现有的主要证明助手中的已验证根计数过程主要基于经典的Sturm定理，该定理仅计数不同的根。在本文中，我们加强了根计数能力在Isabelle/HOL的第一次正式证明布丹-傅立叶定理。随后，基于笛卡尔的符号规则和泰勒移位，我们已经提供了一个验证过程，有效地过近似的实根的数量在一个区间内，计数重。为了准确地计算多重根，我们扩展了我们以前的Sturm定理的形式化。最后，我们结合验证组件在上述发展，以改善我们以前的认证复根计数程序的基础上柯西指数。我们相信这些经过验证的例程对于认证程序和构建策略至关重要。
2018-11-27 cs.LO
Isabelle's Metalogic: Formalization and Proof Checker
Isabelle是一个通用的定理证明器，使用高阶逻辑的一个片段作为定义对象逻辑的元逻辑。伊莎贝尔还提供了证明条件。我们正式这个元逻辑和语言的证明条款在Isabelle/HOL，定义一个可执行的（但效率低下）证明条款检查器，并证明其正确性w.r.t.元逻辑我们将证明检查器与Isabelle集成，并在一系列逻辑和理论上运行它，以检查这些理论中所有证明的正确性。
2021-04-25 cs.LO
Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL
信息物理和机器人系统的形式化验证要求我们能够准确地对现实世界中存在的物理量进行建模。在这些量中使用显式单位可以允许更高程度的严格性，因为我们可以确保计算中量的兼容性。同时，单位的不当使用可能是安全的障碍，因此非常希望在物理计算中进行自动化的健全性检查。在本文中，我们贡献了一个机械化的国际单位制（ISQ）和相关的国际单位制在伊莎贝尔/HOL。我们展示了如何伊莎贝尔可以用来提供一个类型系统的物理量，和自动化的证明支持。向量由对应于基向量的维度类型参数化，因此只有相同维度的量才能相等。由于基本的“量的代数”诱导的数量和SI类型的一致性，具体的战术支持开发，以捕捉这些。我们的建设验证了一个测试集的数量和SI单位之间的已知等价。此外，所提出的理论可以用于SI系统和其他系统（如英国帝国系统（BIS））之间的类型安全转换。
2023-02-15 cs.LO
Interaction with Formal Mathematical Documents in Isabelle/PIDE
Isabelle/PIDE作为Isabelle中交互式定理证明的标准Prover IDE已经出现了10多年。完善的形式证明档案（AFP）证明了形式化数学在Isabelle/HOL中的成功应用。最近，PIDE的范围已经扩大到与Isabelle中的逻辑和证明无关的语言，而是从计算机上更广泛的数学库中提取的。本文件提供了一个总体概述的PIDE项目及其底层的文档模型，内置的并行评估和异步交互。也有一些关于最初的目标和方法、成功和失败、后来对计划的修改以及对未来的想法的讨论。
2019-05-05 cs.LO
A Construction of the Lie Algebra of a Lie Group in Isabelle/HOL
本文在定理证明器 Isabelle 中形式化了光滑向量场、Lie 群及其 Lie 代数，弥补了形式化数学库在微分几何方面的不足，并探讨了与 HOL 简单类型理论集成的挑战。
2024-07-27 cs.LO
Formalizing MLTL Formula Progression in Isabelle/HOL
本文在Isabelle/HOL中形式化了MLTL的语法、语义、关键属性库及公式推进算法，并验证其正确性与可执行性。
2025-02-27 cs.LO
A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle
一个伊莎贝尔/HOL形式化哥德尔的两个不完全定理。这项工作遵循Zeriwierczkowski的详细证明定理使用遗传有限（HF）集理论。避免通常的算术编码的语法消除了形式化的必要性，在嵌入式逻辑演算的初等数论。伊莎贝尔形式化使用两个单独的治疗变量绑定：标称包的规模，以发展这种复杂性，而德Bruijn指数原来是理想的编码语法。伊莎贝尔证明的关键细节进行了描述，特别是在文献中发现的差距和错误。
2021-04-28 cs.LO
A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the $λβ$-calculus in Nominal Isabelle
我们提出了一个简短的证明的Church-Rosser性质的Escherda演算享有两个显着的特点：首先，它采用了Z-属性，从而在一个简短而优雅的证明;其次，它是形式化的名义高阶逻辑可用的证明助手Isabelle/HOL。
2016-09-11 cs.LO
A Formalization of the Semantics of Functional-Logic Programming in Isabelle
现代函数逻辑程序设计语言（如Toy或Curry）具有非严格的非确定性函数，这些函数在调用时选择语义下运行。这种语义的标准公式是CRWL逻辑，它指定了一个证明演算来计算每个表达式的可能结果集。在本文中，我们提出了一个形式化的演算在伊莎贝尔/HOL证明助手。我们已经证明了CRWL的一些基本性质：C-替换下的封闭性，极性和组合性。我们还讨论了已经获得的一些见解，如事实上，左线性的程序规则是不需要任何这些结果举行。
2009-08-04 cs.LO
Making Isabelle Content Accessible in Knowledge Representation Formats
众所周知，像Isabelle、Coq、HOL这样的证明助手库很难被外部工具解释：事实上，只有证明器本身才能充分解析和处理它们。在Isabelle的案例中，作者在1999年就已经设想了将库导出为FAIR（可查找、可解释、可互操作和可重用）知识交换格式，但之前被证明过于困难。在对Isabelle Prover IDE（PIDE）和OMDoc/Mmt格式进行了实质性改进之后，我们现在能够提供这样的导出。具体来说，我们提出了一个集成的PIDE和MMT，允许导出所有的伊莎贝尔库OMDoc格式。我们的出口涵盖了完整的Isabelle发行版和正式证明档案（AFP）-超过12000个理论和地区，产生了超过65GB的OMDoc/XML。将Isabelle内容系统地导出为定义良好的交换格式（如OMDoc）可以支持许多应用程序，如依赖项管理、独立证据检查或库搜索。
2020-05-05 cs.LO
Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
该研究在Isabelle/HOL中机械化实现交互树，构建统一的模型执行与演绎验证框架，可支持多种程序与系统模型的验证及动画生成，保障执行与证明结果一致性。
2024-10-30 cs.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
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
我们在定理证明器Isabelle/HOL中形式化了一个多元量词消去（QE）算法。我们的算法是完整的，因为它能够减少任何量化的公式在一阶逻辑的实算术到一个逻辑等价的量词自由公式。我们形式化的算法是Tarski的原始QE算法和Ben-Or，Kozen和Reif算法的混合，它是第一个完整的多元QE算法形式化的Isabelle/HOL。
2022-12-20 cs.LO math.AG
Infinite Words and Morphic Languages Formalized in Isabelle/HOL
我们提出了一个形式化的基本知识，无限的话，在通用的证明助手伊莎贝尔/HOL。此外，我们提出了一个形式化的纯形态和形态语言。最后，我们提出了一个形式化的定义Sturmian词作为低机械词，并证明了一些非常基本的事实。形式化是基于一个正在进行的更大的项目的形式化组合的话。
2023-03-20 cs.FL cs.LO
Comparison of Two Theorem Provers: Isabelle/HOL and Coq
对数学基础的正式定义的需要在上个世纪出现了。数学的规模和复杂性，以及发现的悖论，揭示了跨理论积累错误的危险。虽然根据哥德尔的不完备性定理，不可能建立一个单一的形式系统来描述世界上所有的现象，同时是完整和一致的，但它产生了相当实用的逻辑领域，例如自动定理证明理论。这是一套用于使用逻辑推理机械地验证数学语句的技术。此外，它还可以用于解决复杂的工程问题，例如，证明软件系统或算法的安全性。本文比较了两个广泛使用的自动定理证明工具，Isabelle/HOL和Coq，在表达能力，局限性和可用性。为此，首先简要介绍了形式系统和自动演绎理论的基础，它们的主要问题和挑战，然后详细比较了所选定理证明器的最显着特征，并提供了说明性的证明示例。
2018-09-06 cs.LO
Stalnaker's Epistemic Logic in Isabelle/HOL
本文在证明助手 Isabelle/HOL 中形式化了针对可数无穷多智能体的认知逻辑 S4.2 的可靠性与完备性结果，并形式化了 S4 两种公理化的等价性，从而巩固了 Stalnaker 知识与信念系统的逻辑基础。
2024-04-23 cs.LO
A Verified Implementation of B+-Trees in Isabelle/HOL
在本文中，我们提出了无处不在的B+树数据结构的交互式定理证明器Isabelle/HOL的强制性实现的验证。该实现支持成员资格测试，插入和范围查询与有效的二进制搜索节点内导航。命令式实现的验证分为两个步骤：一个抽象的集合接口被细化为一个可执行的，但效率低下的纯功能的实现，这是进一步细化为有效的命令式实现。
2022-08-18 cs.DS 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
Certified Quantum Computation in Isabelle/HOL
在这篇文章中，我们提出了一个正在进行的努力，正式量子算法和结果在量子信息论使用的证明助手伊莎贝尔/HOL。形式化方法对于算法和协议的安全性至关重要，我们预见它们在未来将广泛用于量子计算。我们已经开发了一个大型图书馆的量子计算在伊莎贝尔的基础上的矩阵表示的量子电路，成功地正式的无克隆定理，量子隐形传态，Deutsch的算法，Deutsch-Jozsa算法和量子囚徒困境。我们讨论的设计选择，并报告我们在量子博弈论领域的工作成果。
2020-12-27 cs.LO quant-ph
Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL
狭义相对论是现代物理理论的基石。虽然标准坐标模型是众所周知的，并且今天被广泛教导，但存在几种替代的公理系统。本文报告的形式化的一个这样的系统，这是更接近的精神希尔伯特的公理化的方法，以欧几里德几何比向量空间的方法采用闵可夫斯基。我们在Isabelle/HOL中提出了公理系统的机械化以及与时间顺序相关的定理。Isabelle/Isar脚本的证明和摘录进行了讨论，特别是在正式的工作需要额外的步骤，替代方法，或更正舒茨的散文。
2021-09-06 cs.LO gr-qc
Systematic Verification of the Modal Logic Cube in Isabelle/HOL
Freie Universität Berlin（柏林自由大学）；Cambridge University（剑桥大学）
我们提出了一个著名的模态逻辑立方体在Isabelle/HOL的自动验证，在其中我们证明了立方体的逻辑之间的包含关系，使用自动推理工具。先前的工作解决了这个问题，但不限于模态逻辑立方体，并使用一阶逻辑中的编码与一阶自动定理证明器相结合。相比之下，我们的解决方案更优雅，透明和有效。它采用了嵌入的量化模态逻辑在经典的高阶逻辑。自动推理工具，如大锤与LEO-II，Satallax和CVC 4，Metis和Nitpick，实现完全自动化。虽然成功，实验也激励一些技术改进的Isabelle/HOL工具。
2015-07-31 cs.AI cs.LO
Towards United Reasoning for Automatic Induction in Isabelle/HOL
CIIRC, Czech Technical University in Prague（捷克布拉格技术大学捷克信息学、机器人学与控制论研究所）；University of Innsbruck（因斯布鲁克大学）
归纳定理证明是计算机科学中一个重要的长期挑战。在这个扩展的摘要中，我们首先总结了Isabelle/HOL的归纳证明的最新发展。然后，我们提出了联合推理，一种新的方法，进一步自动化归纳定理证明。联合推理成功后，综合运用演绎推理、归纳推理和归纳推理三种推理方法的优点，自动证明困难的归纳问题。
2020-05-25 cs.AI cs.LO
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
Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
我们正式在证明助手伊莎贝尔重要的基本概念和结果在金融数学。我们提供了通用的正式定义的概念，如市场，投资组合，衍生产品，套利或公平的价格，我们表明，在通常的无套利条件下，存在一个复制的投资组合的衍生工具意味着后者承认一个唯一的公平价格。然后，我们提供了Cox-Rubinstein模型的形式化，我们证明了在这个模型中市场是完全的，即，每一个衍生产品都有一个可复制的投资组合。这意味着在这个模型中，每一个衍生产品都有一个唯一的公平价格。
2018-08-10 cs.LO q-fin.PR
L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
本文在Isabelle/HOL中完整形式化了L-mosaics与有界并半格等价性的对象部分，采用AI辅助方法验证了主要理论结果及变换互逆性，展示了多值代数运算深度与AI增强定理证明的潜力。
2025-09-24 cs.LO math.AC
PaMpeR: Proof Method Recommendation System for Isabelle/HOL
Czech Technical University in Prague（布拉格捷克理工大学）；University of Innsbruck（因斯布鲁克大学）；University of Sydney（悉尼大学）
决定哪个子工具用于给定的证明状态需要每个ITP特有的专业知识。为了缓解这个问题，我们提出了PaMpeR，Isabelle/HOL的证明方法推荐系统。给定一个证明状态，PaMpeR推荐证明方法来实现证明目标，并提供定性解释说明为什么它建议这些方法。PaMpeR基于现有的手写证明语料库生成这些建议，从而将经验丰富的用户的专业知识转移给新用户。我们的评估表明，PaMpeR正确地预测有经验的用户的证明方法调用，特别是当它涉及到特殊用途的证明方法。
2018-06-19 cs.AI cs.LO
Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL
该研究在 Isabelle/HOL 中完成了 STARK 风格透明证明协议的形式化，构建了含证明者/验证者可执行模型等内容的开发成果，为相关领域提供了形式化方法层面的支撑。
2026-09-23 cs.LO cs.SE
