Natural Deduction and the Isabelle Proof Assistant
我们描述了我们的自然演绎助手（NaDeA）和Isabelle证明助手和NaDeA之间的接口。特别是，我们解释了如何NaDeA，使用生成的证明，已在伊莎贝尔验证，提供反馈给学生，以及如何NaDeA，每个公式证明的学生，提供了一个生成的定理，可以在伊莎贝尔验证。
2018-03-05 cs.LO
TLA+ Proofs
TLA+是一种基于标准集合论和时态逻辑的规约语言，具有用于分层证明的构造。我们描述了如何编写TLA+证明并使用TLAPS（TLA+证明系统）进行检查。我们使用彼得森的互斥算法作为一个简单的例子来描述TLAPS的功能，并展示它和TLAPS（TLA+的IDE）如何帮助用户管理大型，复杂的证明。
2012-08-29 cs.LO cs.SE
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
在同一问题的形式化上比较证明者总是一个有价值的练习。在本文中，我们提出了一个非平凡的算法的正确性的形式证明，从图论中进行了三个证明助手：Why3，Coq和Isabelle。
2018-10-29 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
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
Reconstructing veriT Proofs in Isabelle/HOL
自动定理证明器现在通常用于交互式定理证明器中，以履行越来越多的证明义务。为了保持证明的可信度，必须在证明助手中验证自动找到的证明。我们在这里提出了一个重建过程中的证明助手Isabelle/HOL证明生成的可满足性模理论求解器veriT这是smt策略的一部分。我们详细描述了我们改进的重建方法的架构和我们在设计它时所面临的挑战。我们的实验表明，VeriT驱动的SMT策略经常被Sledgehammer建议为自动解决证明目标的最快方法。
2019-08-26 cs.LO
Homotopy Type Theory in Isabelle
本文介绍了Isabelle/HoTT，同伦类型论的第一个发展Isabelle证明助手。在Paulson早期工作的基础上，我使用Isabelle现有的逻辑框架基础设施来实现基本的自动化，例如类型检查和术语细化，这通常是在依赖类型系统的源代码级别上处理的。我还集成了命题作为类型的范式与声明性的Isar证明语言，提供了一种替代的Coq和Agda的证明条款的基于策略的证明。基础设施开发，然后用于形式化的同伦类型论书的基础结果。
2021-04-19 cs.LO
Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL
我们形式化和机械化的一个concentive，证明理论的证明克雷格的插值定理在伊莎贝尔/HOL。我们给出了所有的定义和引理声明正式和非正式。我们也非正式地转录形式证明。我们详细介绍了我们的机械化的主要特点，如一阶公式的约束力的形式化。给出了Craig插值定理的一些应用。
2006-07-12 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
Goal-Oriented Conjecturing for Isabelle/HOL
我们提出了PGT，一个证明目标Transformer的Isabelle/HOL。给定一个证明目标及其背景上下文，PGT试图通过转换原始证明目标来从原始目标生成证明。这些构造应该足够弱，可以通过自动化来证明，但又足够强，可以证明最初的目标。通过将PGT到预先存在的PSL框架，我们利用伊莎贝尔的强大的自动化来识别和证明这样的结构。
2018-07-25 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
Getting Started with Isabelle/jEdit in 2018
这是对Isabelle/jEdit（证明助手Isabelle的主用户界面）的面向初学者的介绍。
2019-02-05 cs.LO
Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs
在过去的几年里，伊莎贝尔正式证明档案已经发展到相当大的规模。它弥补了一个令人印象深刻的机构的研究，使一些统计方法的各个方面的定理证明，并尚未被用尽。然而，不断增长的规模也带来了一些挑战：材料变得越来越难找到，可重用性和易于理解变得更加重要。本文总结了我在这些课题上的研究计划，并简要介绍了初步的结果，这些结果表明文档依赖图的节点入度服从无标度分布。
2022-09-27 cs.LO
Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
本文提出一种分析Metis成功证明以提取变量实例化的新工具，从而提升Sledgehammer的成功率与证明速度，并帮助用户理解目标与引理之间的推导关系。
2025-08-28 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
From LCF to Isabelle/HOL
交互式定理证明器在过去的四十年里得到了巨大的发展，从原始的开始到今天的强大系统。在这里，我们专注于Isabelle/HOL及其独特的优势。它们包括自动证明搜索，从一阶定理证明世界借用技术，但也自动搜索反例。它们包括一个高度可读的结构化证明语言和一个独特的交互式开发环境，用于编辑现场证明文档。一切都建立在Robin Milner为Edinburgh LCF设想的基础上：一个证明内核，使用抽象类型来确保可靠性并消除存储证明的需要。与20世纪70年代的研究原型相比，Isabelle是一个实用和通用的工具。它被系统设计师，数学家和许多其他人使用。
2019-07-17 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
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs
我们扩展了混合系统的语义验证框架与Isabelle/HOL证明助手的混合程序存储的代数模型，混合程序及其正确性规范的浅层表达模型，和特定领域的演绎和计算支持。新的存储模型产生干净的分离和变量的动态局部视图，例如离散/连续，可变/不可变，程序/逻辑，以及使用组合子，投影和框架操纵它们的增强方式。这导致了更多的本地推理规则，程序和策略，用于使用不变集进行推理，验证混合规范的解决方案或计算具有增强的证明自动化和可扩展性的导数。新的表达式模型提供了更用户友好的语法，更好的名称空间控制和连接框架与真实世界建模语言的接口。
2021-06-10 cs.LO
The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle/ZF
选择公理的相对一致性的证明已经使用Isabelle/ZF机械化。这个证明建立在反射定理以前的机械化基础上。在原始证明中对元理论的严重依赖使得形式化异常长，并且不完全令人满意：证明的两个部分不适合在一起。如果不将元理论形式化，似乎不可能解决这些问题。然而，目前的发展遵循一个标准的教科书，Kunen的集合论，并可以支持从这本书进一步材料的形式化。它也是一个例子，说明当深度数学形式化时会发生什么。
2021-04-26 cs.LO
Generic Automatic Proof Tools
本书的章节建立了交互式证明工具Isabelle和经典tableau和解析技术之间的联系。伊莎贝尔的经典推理描述和证明了一个扩展的案例研究：教会罗瑟定理的组合。与其他交互式定理证明器相比，Isabelle的经典推理器实现了高度的自动化。
2001-03-29 cs.LO
Translating Scala Programs to Isabelle/HOL
我们提出了一个值得信赖的莱昂验证系统和伊莎贝尔证明助手之间的连接。Leon是一个用于验证Scala程序功能的系统。它使用各种自动定理证明器（ATP）来检查源于输入程序的验证条件（VC）。另一方面，Isabelle是一个交互式定理证明器，用于使用自己的输入语言Isabelle/Isar验证数学规范。用户指定（归纳）定义并手动编写关于它们的证明，尽管有半自动化策略的帮助。这两个系统的集成，使我们能够利用伊莎贝尔丰富的标准库，并给予更大的信心，保证分析程序的正确性。
2016-07-06 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
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
计算机代数和数值分析中的许多问题都可以归结为计算或近似计算一个区间内多项式的实根。现有的主要证明助手中的已验证根计数过程主要基于经典的Sturm定理，该定理仅计数不同的根。在本文中，我们加强了根计数能力在Isabelle/HOL的第一次正式证明布丹-傅立叶定理。随后，基于笛卡尔的符号规则和泰勒移位，我们已经提供了一个验证过程，有效地过近似的实根的数量在一个区间内，计数重。为了准确地计算多重根，我们扩展了我们以前的Sturm定理的形式化。最后，我们结合验证组件在上述发展，以改善我们以前的认证复根计数程序的基础上柯西指数。我们相信这些经过验证的例程对于认证程序和构建策略至关重要。
2018-11-27 cs.LO
Natural Deduction as Higher-Order Resolution
一个交互式定理证明程序Isabelle正在开发中。在LCF中，每个推理规则由一个用于向前证明的函数和另一个用于向后证明的函数（一种策略）表示。在Isabelle中，每个推理规则由Horn子句表示。解析给出了向前和向后的证明，支持一大类逻辑。伊莎贝尔被用来证明马丁-洛夫的构造性类型论中的定理。量词构成了几个困难：替代，约束变量，Skolemization。Isabelle的逻辑语法表示是类型化的微积分，需要更高阶的统一。它可能具有逻辑编程的潜力。沿着推理规则的深度优先子目标构成高阶Prolog。
2000-10-31 cs.LO
On Exams with the Isabelle Proof Assistant
Technical University of Denmark（丹麦技术大学）
我们提出了一种方法来测试学生的学习成果，在自动推理的过程中使用伊莎贝尔证明助手。该方法使我们能够测试一般理解的形式证明在各种逻辑证明系统和理解的证明，特别是在高阶逻辑的伊莎贝尔/HOL。使用Isabelle几乎可以自动对考试的大部分内容进行评分。我们通过一些示例问题来解释我们的方法，并解释为什么我们认为我们选择的每种问题都足以衡量我们预期的学习成果。最后，我们讨论了我们的经验，使用的方法考试的课程自动推理，并建议潜在的未来工作。
2023-03-10 cs.AI cs.LO
Isabelle: The Next 700 Theorem Provers
Isabelle是一个通用的定理证明器，设计用于各种形式理论的交互式推理。目前，它为构造类型论、各种一阶逻辑、Zermelo-Fraenkel集合论和高阶逻辑提供了有用的证明过程。这一调查伊莎贝尔作为一个介绍文学。它解释了为什么一般的定理证明是有益的。它提供了一个彻底的历史伊莎贝尔，从它的起源在LCF系统。它提出了一个帐户的逻辑是如何表示，说明使用经典逻辑。该方法与爱丁堡逻辑框架进行了比较。几个伊莎贝尔对象逻辑。
2000-10-31 cs.LO
A Formalization of the Semantics of Functional-Logic Programming in Isabelle
现代函数逻辑程序设计语言（如Toy或Curry）具有非严格的非确定性函数，这些函数在调用时选择语义下运行。这种语义的标准公式是CRWL逻辑，它指定了一个证明演算来计算每个表达式的可能结果集。在本文中，我们提出了一个形式化的演算在伊莎贝尔/HOL证明助手。我们已经证明了CRWL的一些基本性质：C-替换下的封闭性，极性和组合性。我们还讨论了已经获得的一些见解，如事实上，左线性的程序规则是不需要任何这些结果举行。
2009-08-04 cs.LO
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
A Formulation of the Simple Theory of Types (for Isabelle)
简单的类型论制定使用通用定理证明伊莎贝尔。这需要显式的类型推断规则。有函数、产品和子集类型，它们可以为空。描述（eta运算符）引入了选择公理。高阶逻辑是通过公式和布尔型项之间的反射得到的。递归类型和函数可以正式构造。Isabelle证明程序。逻辑似乎适合一般数学以及计算问题。
2000-10-31 cs.LO
Set Theory for Verification: I. From Foundations to Functions
规范和验证的逻辑来自Zermelo-Fraenkel集合论的公理。使用证明助手Isabelle进行证明。Isabelle是通用的，支持几种不同的逻辑。Isabelle具有适应集合论变体的灵活性。它的高阶语法支持新绑定操作符的定义。子目标中的未知数可以递增地实例化。本文描述了描述、关系和函数的规则的推导，并讨论了Cantor定理、同态合成挑战[9]和Ramsey定理[5]的交互式证明。一个通用的证明助手可以对抗专用于特定逻辑的证明器。
2000-10-31 cs.LO
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
证明助手，如Isabelle/HOL，提供了一些工具来促进归纳定理证明。Isabelle专家知道如何有效地使用这些工具;然而，有一点工具支持将这些专家知识传递给更广泛的用户受众。为了解决这个问题，我们提出了我们的领域特定的语言，LiFtEr。LiFtEr允许有经验的Isabelle用户以独立于任何问题域的风格编码他们的归纳推理。LiFtEr的解释器机械地检查归纳工具的给定应用程序是否与逻辑匹配，从而自动化知识传递循环。
2020-05-24 cs.LO
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL
我们提出了一个证明过程中的Isabelle/HOL的一元实多项式问题。我们的过程的核心数学是基于单变量柱形代数分解。我们遵循不可信证书的方法，将解决与验证分离：高效的外部工具执行昂贵的真实代数计算，产生在Isabelle逻辑中正式检查的证据。这使我们能够利用高度调整的计算机代数系统，如Mathematica来指导我们的过程，而不会影响其结果的正确性。我们目前的实验证明这种方法的有效性，在许多情况下产生的数量级的改进，比以前的方法。
2018-04-10 cs.LO
Towards Evolutionary Theorem Proving for Isabelle/HOL
University of Innsbruck（因斯布鲁克大学）；Czech Technical University（捷克技术大学）
机械化的定理证明正成为可靠系统编程和严格数学的基础。尽管在校样自动化方面取得了数十年的进步，但编写机械化校样仍然需要工程师的专业知识，并且仍然是劳动密集型的。近年来，研究者们利用监督学习从已有的大型证明语料库中提取交互式证明开发的知识。然而，现有的证明语料库只提供了一种证明猜想的方法，而往往有多个等价有效的方法来证明一个猜想。在这篇摘要中，我们确定了发现自动证明搜索算法的挑战，并提出了我们的新方法，以提高在伊莎贝尔/HOL自动证明搜索算法使用演化计算。
2019-04-17 cs.AI cs.LO
Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM
通常需要保证案例来验证关键系统。在保证中使用形式化方法可以提高自动化程度，增加可信度，并克服错误的推理。然而，保证案例永远不能完全形式化，因为正式方法的使用取决于由非正式过程验证的模型。因此，保证技术应该支持正式和非正式的工件，并在它们之间建立明确的推理联系。在本文中，我们贡献了一个正式的机器检查的交互式语言，称为Isabelle/SACM，支持计算机辅助建设符合OMG结构化保证案例元模型的保证案例。Isabelle/SACM的使用保证了保证案例的格式良好、一致性和可追溯性，并允许各种来源的正式和非正式证据的紧密集成。特别是，Isabelle带来了各种可以提供证据的自动验证技术。为了验证我们的方法，我们提出了一个基于Tokeneer安全进入系统基准的大量案例研究。我们将其功能规范嵌入到Isabelle中，验证其安全需求，并在Isabelle/SACM中形成一个模块化的安全案例，该案例结合了异构工件。因此，我们表明，伊莎贝尔是一个合适的平台，关键系统保证。
2020-09-25 cs.LO cs.SE
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
Teaching Higher-Order Logic Using Isabelle
Technical University of Denmark（丹麦技术大学）
本文基于 Isabelle/Pure 构建了一个小巧可读的高阶逻辑形式化，提供示例证明、公理规则说明及课堂教学经验，作为学习证明助手的轻量入门。
2024-04-08 cs.AI 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
Attack Trees in Isabelle
在本文中，我们提出了一个证明理论的攻击树。攻击树是一种建立良好的和有用的模型，用于构建对系统的攻击，因为它们允许在应用场景中逐步探索高级攻击。利用Isabelle中高阶逻辑的表达能力，我们成功地开发了一种基于Kripke结构和CTL的基于状态语义的通用攻击树理论。由此产生的框架允许机械支持的逻辑分析的元理论的攻击树的证明演算，并在同一时间开发的证明理论，使应用到案例研究。中心的正确性和完整性的结果证明在伊莎贝尔建立了攻击树的有效性和CTL的概念之间的联系。该应用程序以医疗物联网系统和GDPR合规性验证为例进行说明。
2018-05-15 cs.CR cs.LO
NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
我们提出了一个新的软件工具，用于教学逻辑的基础上自然演绎。它的证明系统在证明助手Isabelle中得到了形式化的描述，使得它的定义非常精确。形式化的合理性已在Isabelle中得到证明。该工具是用TypeScript / JavaScript开发的开源软件，因此可以直接在浏览器中使用，无需进一步安装。虽然开发的本科计算机科学的学生谁是用来学习和编程具体的计算机代码在程序设计语言，我们认为相关的方法为更广泛的受众和其他证明系统。
2015-07-14 cs.CY cs.LO
Beginners' Quest to Formalize Mathematics: A Feasibility Study in Isabelle
使用交互式定理证明器有多难？我们的回应，审查形式化的希尔伯特的第十个问题在伊莎贝尔/HOL进行的本科生研究小组在雅各布斯大学不来梅。我们认为，我们的例子表明，证明助手是可行的初学者形式化数学。为了使该领域更容易访问，我们还调查了学习交互式定理证明器时出现的障碍。从广义上讲，我们主张在数学研究和课程中更多地采用交互式定理证明器。
2021-06-23 cs.LO
Template-Based Conjecturing for Automated Induction in Isabelle/HOL
归纳证明在形式化验证中起着核心作用。然而，它的自动化仍然是计算机科学的一个巨大挑战。为了解决归纳问题，人类工程师经常需要手动提供辅助引理。我们自动化这个费力的过程与基于模板的推理，一种新的方法来生成辅助引理，并用它们来证明最终目标。我们的评估表明，我们的工作原型，TBC，实现了40个百分点的成功率提高中等难度的问题。
2023-01-19 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
Isabelle/HOL as a Meta-Language for Teaching Logic
证明助手是逻辑教学的重要工具。我们支持这一主张，讨论三个形式化的Isabelle/HOL在最近的课程中使用的自动推理。第一个是系统W（一个只有两个原始符号的经典命题逻辑系统）的形式化，第二个是自然演绎助手（NaDeA），第三个是使用我们的序列演算验证器（SeCaV）的单边递归演算。我们依次描述每个形式化，集中在我们如何在教学中使用它们，并从逻辑教育的角度评论有趣或有用的功能。最后，我们反思了所吸取的经验教训，以及这些经验教训下一步可能引导我们走向何方。
2020-10-30 cs.LO
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
Czech Technical University in Prague（布拉格捷克理工大学）；University of Innsbruck（因斯布鲁克大学）
最近，越来越多的研究人员已经应用机器学习来帮助交互式定理证明器的用户。然而，底层逻辑的表达性和证明文档的深奥结构阻碍了机器学习从业者，他们通常在形式逻辑方面没有太多的专业知识，更不用说Isabelle/HOL了，无法在这一领域取得大规模的成功。在这个数据描述中，我们提出了一个简单的数据集，其中包含超过40万个证明方法应用程序的数据，以及每个应用程序的100多个提取特征，这些特征的格式可以在没有任何形式逻辑知识的情况下轻松处理。我们简单的数据格式允许机器学习从业者尝试机器学习工具来预测Isabelle/HOL中的证明方法，而不需要逻辑领域的专业知识。
2020-05-26 cs.AI cs.DB cs.LG
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
广义集合论（GST）类似于标准集合论，但也可以有非集合结构化对象，这些非集合结构化对象可以包含其他结构化对象，包括集合。本文介绍了对GST的Isabelle/HOL支持，GST被视为组合了指定各种数学对象的特征的类型类，例如，集合、序数、函数等。GST可以具有一个异常特征，该异常特征简化了部分函数和未定义性的表示。在组装GST时，根据用户可修改的策略生成额外的公理以填补规范空白。被称为软类型的特殊类型谓词被广泛使用。虽然GST可以在没有模型的情况下使用，但为了确保其一致性，我们从组件中为每个GST构建一个模型，该组件指定每个功能对通过顺序递归定义的冯诺依曼式累积层次结构的每一层的贡献，然后我们将模型连接到GST占用的单独类型。
2022-07-25 cs.LO math.LO
Towards Mechanised Proofs in Double-Pushout Graph Transformation
我们正式的双推出的方法，图变换的基础知识，在证明助手伊莎贝尔/HOL，并提供相关的机器检查证明。具体来说，我们正式的图形，图形态射和规则，并定义直接派生的基础上删除和胶合。然后，我们正式的图形推出和证明与伊莎贝尔的帮助下，删除和胶合推。我们还证明了推出是唯一的同构。格式包括大约2000行源文本。我们的动机是铺平道路，严格的，机器检查证明的理论的双重推出的方法，并奠定了基础，验证图形转换系统和基于规则的图形程序的交互式定理证明。
2022-12-22 cs.LO
Infinite Words and Morphic Languages Formalized in Isabelle/HOL
我们提出了一个形式化的基本知识，无限的话，在通用的证明助手伊莎贝尔/HOL。此外，我们提出了一个形式化的纯形态和形态语言。最后，我们提出了一个形式化的定义Sturmian词作为低机械词，并证明了一些非常基本的事实。形式化是基于一个正在进行的更大的项目的形式化组合的话。
2023-03-20 cs.FL cs.LO
Isabelle/PIDE as Platform for Educational Tools
Université Paris-Sud 11（巴黎第十一大学）
Isabelle/PIDE平台解决了LCF系列的证明助手是否适合作为教育工具的技术基础的问题。像HOL、Coq或Isabelle这样的系统传统上强大的逻辑基础到目前为止已经被TTY（或像著名的Proof General / Emacs接口这样的小变体）的一些不可访问的交互所抵消。因此，数学教育工具与完全正式的背景理论的基本问题，往往是否定的回答，由于现有的证明引擎偶然的弱点。“PIDE”（意为“ProverIDE”）的理念是将现有的证明器（如Isabelle）集成到一个更大的环境中，以方便最终用户和其他工具的访问。我们使用Scala将ML中的证明引擎公开给JVM世界，那里已经存在许多用户界面、编辑器框架和教育工具。这将最终导致组合数学助手，其中逻辑引擎是在后台，而不妨碍形式化方法，形式化数学，特别是数学教育的应用程序的看法。
2012-02-22 cs.AI cs.LO cs.MS
Stalnaker's Epistemic Logic in Isabelle/HOL
本文在证明助手 Isabelle/HOL 中形式化了针对可数无穷多智能体的认知逻辑 S4.2 的可靠性与完备性结果，并形式化了 S4 两种公理化的等价性，从而巩固了 Stalnaker 知识与信念系统的逻辑基础。
2024-04-23 cs.LO
The Foundation of a Generic Theorem Prover
Isabelle是一个交互式定理证明器，支持各种逻辑。它将规则表示为命题（而不是函数），并通过组合规则来构建证明。这些操作构成了一个元逻辑（或“逻辑框架”），其中对象逻辑被形式化。伊莎贝尔现在是基于高阶逻辑-一个精确和良好理解的基础。示例说明了使用此元逻辑来形式化逻辑和证明。一阶逻辑的公理被证明是可靠和完备的。后向证明通过关于对象级蕴涵的元推理形式化。高阶逻辑比其他元逻辑有几个实际的优势。许多证明技术是已知的，如休特的高阶统一程序。
2000-10-31 cs.LO
Domain-Specific Language to Encode Induction Heuristics
证明助手，如Isabelle/HOL，提供了一些工具来促进归纳定理证明。Isabelle专家知道如何有效地使用这些工具;然而，他们没有系统的方法来编码他们的专业知识。为了解决这个问题，我们提出了我们的领域特定的语言，LiFtEr。LiFtEr允许有经验的Isabelle用户以独立于任何问题域的风格编码他们的归纳推理。LiFtEr的解释器机械地检查归纳工具的给定应用是否与有经验的用户指定的知识相匹配，从而系统地将有经验的用户的专业知识传递给新的Isabelle用户。
2019-06-29 cs.LO
CAPRI: Contract-Aware Proof Repair for Isabelle
Southwest University（西南大学）；Aarhus University（奥胡斯大学）；University of York（约克大学）；Centro de Informática, Universidade Federal de Pernambuco (UFPE)（伯南布哥联邦大学信息中心）；University of Lancaster（兰卡斯特大学）
该研究提出CAPRI工具，用于解决Isabelle证明修复中LLM修改未授权内容的问题，通过契约检查机制保障安全，在12个失败证明的实验中验证了不同工作流的修复效果。
2026-08-14 cs.AI cs.LO cs.SE
Interactive Simplifier Tracing and Debugging in Isabelle
Isabelle证明助手配备了一个非常强大的术语简化策略。虽然非常有用，但简化术语的结果并不总是与用户的期望相匹配：有时，所得到的术语不是用户期望的形式，或者简化器未能应用规则。我们描述了一个新的，交互式的跟踪设施，它提供了深入了解的层次结构的简化与用户定义的过滤，memoization和搜索。新的验证器跟踪集成到Isabelle/jEdit Prover IDE中。
2014-06-02 cs.LO cs.MS
