Formalization of Forcing in Isabelle/ZF
我们形式化的强迫理论的集合论框架中的Isabelle/ZF。在ZFC的可数传递模型存在的假设下，构造了一个适当的通有扩张，并证明了后者也满足ZFC。在这样做的过程中，我们对Paulson的ZF-可构造性库进行了重新设计。
2020-04-18 cs.LO math.LO
Isabelle/HOL as a Meta-Language for Teaching Logic
证明助手是逻辑教学的重要工具。我们支持这一主张，讨论三个形式化的Isabelle/HOL在最近的课程中使用的自动推理。第一个是系统W（一个只有两个原始符号的经典命题逻辑系统）的形式化，第二个是自然演绎助手（NaDeA），第三个是使用我们的序列演算验证器（SeCaV）的单边递归演算。我们依次描述每个形式化，集中在我们如何在教学中使用它们，并从逻辑教育的角度评论有趣或有用的功能。最后，我们反思了所吸取的经验教训，以及这些经验教训下一步可能引导我们走向何方。
2020-10-30 cs.LO
NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
我们提出了一个新的软件工具，用于教学逻辑的基础上自然演绎。它的证明系统在证明助手Isabelle中得到了形式化的描述，使得它的定义非常精确。形式化的合理性已在Isabelle中得到证明。该工具是用TypeScript / JavaScript开发的开源软件，因此可以直接在浏览器中使用，无需进一步安装。虽然开发的本科计算机科学的学生谁是用来学习和编程具体的计算机代码在程序设计语言，我们认为相关的方法为更广泛的受众和其他证明系统。
2015-07-14 cs.CY 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
The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle/ZF
选择公理的相对一致性的证明已经使用Isabelle/ZF机械化。这个证明建立在反射定理以前的机械化基础上。在原始证明中对元理论的严重依赖使得形式化异常长，并且不完全令人满意：证明的两个部分不适合在一起。如果不将元理论形式化，似乎不可能解决这些问题。然而，目前的发展遵循一个标准的教科书，Kunen的集合论，并可以支持从这本书进一步材料的形式化。它也是一个例子，说明当深度数学形式化时会发生什么。
2021-04-26 cs.LO
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
在同一问题的形式化上比较证明者总是一个有价值的练习。在本文中，我们提出了一个非平凡的算法的正确性的形式证明，从图论中进行了三个证明助手：Why3，Coq和Isabelle。
2018-10-29 cs.LO
Quantum projective measurements and the CHSH inequality in Isabelle/HOL
我们提出了一个形式化的Isabelle/HOL的量子投影测量，一类测量涉及正交投影仪，经常用于量子计算。我们还形式化了CHSH不等式，这一结果在任意概率空间都成立，可以用来反驳量子力学中局部隐变量理论的存在性。
2021-03-15 cs.LO
FindFacts: A Scalable Theorem Search
伊莎贝尔正式证明档案（AFP）在2019年底已经增长到500多篇文章。与此同时，在其中找到形式化并没有变得更容易。在撰写本文时，网站特定的AFP谷歌搜索和伊莎贝尔发现理论分别。find_consts命令（仅适用于导入的理论）仍然是Isabelle中唯一可用的形式化工具。我们提出FindFacts，一个新的特定领域的搜索工具，正式伊莎贝尔理论的内容。而不是利用长期统一，我们解决了一个经典的钻取下搜索引擎的问题。我们特别强调的可扩展性的搜索系统，使整个AFP可以交互式搜索。
2022-04-27 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
A Formalization of Martingales in Isabelle/HOL
本文在Isabelle/HOL中形式化了任意巴拿赫空间上的鞅理论，将条件期望从实数推广到巴拿赫空间，定义了随机过程及鞅类，并证明了平均定理以确立密度的唯一性。
2023-11-10 cs.LO math.PR
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
Complex Bounded Operators in Isabelle/HOL
RWTH Aachen（亚琛工业大学）；University of Tartu（塔尔图大学）；Université Laval（拉瓦尔大学）
本文在Isabelle/HOL中形式化了复向量空间上的有界算子，包括复范数空间、巴拿赫空间、希尔伯特空间，定义了有界算子类型cblinfun，并发展了酉算子、投影算子、有界线性函数延拓定理、伴随算子、Loewner序、闭子空间等理论，同时为有限维情况提供了与矩阵的代码生成支持。
2026-05-31 cs.LO
L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
本文在Isabelle/HOL中完整形式化了L-mosaics与有界并半格等价性的对象部分，采用AI辅助方法验证了主要理论结果及变换互逆性，展示了多值代数运算深度与AI增强定理证明的潜力。
2025-09-24 cs.LO math.AC
Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL
该研究在 Isabelle/HOL 中完成了 STARK 风格透明证明协议的形式化，构建了含证明者/验证者可执行模型等内容的开发成果，为相关领域提供了形式化方法层面的支撑。
2026-09-23 cs.LO cs.SE
Natural Deduction Assistant (NaDeA)
我们提出了自然演绎助手（NaDeA），并讨论了它的优点和缺点作为一种工具，用于教学逻辑。NaDeA可在线获得，基于Isabelle证明助手中的自然演绎的形式化。我们首先提供简洁的配方的主要形式化结果。然后，我们详细说明的先决条件NaDeA，特别是我们描述了一个形式化的伊莎贝尔的“希尔伯特公理”，我们使用作为一个起点，在我们的本科课程数理逻辑。我们讨论了最近的评估NaDeA，并给出了一个概述在NaDeA的练习。
2019-04-01 cs.LO
Teaching Intuitionistic and Classical Propositional Logic Using Isabelle
我们描述了一个自然演绎形式化的直觉和经典命题逻辑的伊莎贝尔/纯框架。与早期的工作相比，我们探索了使用深度嵌入方法进行逻辑建模的教学优势，在这里我们采用了逻辑框架建模。这产生了简单而自然的教学例子，我们报告了它在2020年和2021年教授我们的自动推理课程中所发挥的作用。
2022-02-08 cs.LO
Isabelle: The Next 700 Theorem Provers
Isabelle是一个通用的定理证明器，设计用于各种形式理论的交互式推理。目前，它为构造类型论、各种一阶逻辑、Zermelo-Fraenkel集合论和高阶逻辑提供了有用的证明过程。这一调查伊莎贝尔作为一个介绍文学。它解释了为什么一般的定理证明是有益的。它提供了一个彻底的历史伊莎贝尔，从它的起源在LCF系统。它提出了一个帐户的逻辑是如何表示，说明使用经典逻辑。该方法与爱丁堡逻辑框架进行了比较。几个伊莎贝尔对象逻辑。
2000-10-31 cs.LO
Formalization of Differential Privacy in Isabelle/HOL
本文提出一个通用的 Isabelle/HOL 差分隐私形式化库，首次支持连续概率分布，并验证了标准定义、Laplace 机制和 report noisy max 机制。
2024-10-20 cs.CR cs.LO cs.PL
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
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
我们提出了简单的新的霍尔逻辑和精化演算的混合系统的风格的微分动态逻辑。（细化）Kleene代数与测试用于推理程序结构和生成验证条件在这一级。透镜以通用代数方式捕获混合程序存储。该方法已正式与伊莎贝尔/霍尔证明助手。一些示例解释了工作流程和最终的验证组件。
2019-10-29 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
Formalization of the fundamental group in untyped set theory using auto2
我们提出了一个新的框架，形式化数学在无类型集合论使用auto 2。使用这个框架，我们正式在伊莎贝尔/FOL的整个链的发展，从公理集理论的定义的基本组为任意拓扑空间。auto 2 prover被用作唯一的自动化工具，并在整个项目中启用简洁的证明脚本。
2017-07-15 cs.LO
Concrete Semantics with Coq and CoqHammer
“具体语义学”一书介绍了伴随着Isabelle/HOL形式化的命令式程序设计语言。在本文中，我们讨论了重新形式化的书使用Coq证明助手。为了实现类似的简洁的正式文本，我们广泛使用CoqHammer以及Coq Ltac级别的自动化。我们比较的形式化效率，紧凑性和可读性的证明脚本源于一个Coq重新形式化的两章书。
2018-08-20 cs.LO
A Formulation of the Simple Theory of Types (for Isabelle)
简单的类型论制定使用通用定理证明伊莎贝尔。这需要显式的类型推断规则。有函数、产品和子集类型，它们可以为空。描述（eta运算符）引入了选择公理。高阶逻辑是通过公式和布尔型项之间的反射得到的。递归类型和函数可以正式构造。Isabelle证明程序。逻辑似乎适合一般数学以及计算问题。
2000-10-31 cs.LO
Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs
由于Avenhaus和Loría-Sáenz，我们提出了一个Isabelle/HOL形式化的准还原强确定性条件项重写系统的汇流特性。
2016-09-12 cs.LO
Stalnaker's Epistemic Logic in Isabelle/HOL
本文在证明助手 Isabelle/HOL 中形式化了针对可数无穷多智能体的认知逻辑 S4.2 的可靠性与完备性结果，并形式化了 S4 两种公理化的等价性，从而巩固了 Stalnaker 知识与信念系统的逻辑基础。
2024-04-23 cs.LO
Formalizing MLTL Formula Progression in Isabelle/HOL
本文在Isabelle/HOL中形式化了MLTL的语法、语义、关键属性库及公式推进算法，并验证其正确性与可执行性。
2025-02-27 cs.LO
Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?
当面对如何在形式证明系统中表示属性的问题时，任何用户都必须做出设计决策。我们已经证明了三个定理，从马斯金的2004年调查文章拍卖理论使用伊莎贝尔/HOL系统，我们已经产生了验证代码的组合Vickrey拍卖。一个基本的问题是如何表示一些基本概念：由于集合论在Isabelle/HOL中可用，当引入新的定义时，通常会出现平衡集合论对象和使用更典型的高阶逻辑（如函数或列表）表示的对象的数量的问题。同样，用户经常必须回答是否使用建设性定义或非建设性定义的问题。这样的决定有后果的证明发展和可用性的形式化。例如，集合通常更接近经济学家使用和识别的表示，而其他对象更接近计算内容的提取。在本文中，我们给出了这些方法的优点和缺点及其关系的例子。此外，我们提出了相应的伊莎贝尔图书馆的定义和定理，最突出的是那些处理关系和约束。
2014-06-01 cs.LO
Natural Deduction as Higher-Order Resolution
一个交互式定理证明程序Isabelle正在开发中。在LCF中，每个推理规则由一个用于向前证明的函数和另一个用于向后证明的函数（一种策略）表示。在Isabelle中，每个推理规则由Horn子句表示。解析给出了向前和向后的证明，支持一大类逻辑。伊莎贝尔被用来证明马丁-洛夫的构造性类型论中的定理。量词构成了几个困难：替代，约束变量，Skolemization。Isabelle的逻辑语法表示是类型化的微积分，需要更高阶的统一。它可能具有逻辑编程的潜力。沿着推理规则的深度优先子目标构成高阶Prolog。
2000-10-31 cs.LO
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
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
Teaching Higher-Order Logic Using Isabelle
Technical University of Denmark（丹麦技术大学）
本文基于 Isabelle/Pure 构建了一个小巧可读的高阶逻辑形式化，提供示例证明、公理规则说明及课堂教学经验，作为学习证明助手的轻量入门。
2024-04-08 cs.AI cs.LO
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
我们提出了一个框架，在Isabelle验证渐近时间复杂度的命令式程序。我们建立在命令HOL及其分离逻辑的扩展之上，以包括运行时间。除了基本的参数，我们的框架能够处理先进的技术，时间复杂度分析，如使用Akra-Bazzi定理和摊还分析。各种自动化的建立和纳入自动2证明的原因与时间信用的分离逻辑，并得出渐近行为的功能。作为案例研究，我们验证了渐进的时间复杂度（除了功能的正确性）的命令式算法和数据结构，如中位数的中位数选择，Karatsuba的算法，和splay树。
2018-02-05 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
Confluence by Decreasing Diagrams -- Formalized
本文给出了定理证明器Isabelle中递减图的形式化。它讨论了机械证明，表明任何局部减少的抽象重写系统是合流。考虑了谷值和递减图的转换形式。
2013-04-11 cs.LO
Predicate Transformer Semantics for Hybrid Systems: Verification Components for Isabelle/HOL
我们提出了一个语义框架的演绎验证的混合系统与Isabelle/HOL。它支持推理的时间演化的混合程序的差分动态逻辑建模的流或向量场的不变集的风格。我们介绍了这个框架的语义基础，并总结了他们的伊莎贝尔形式化以及由此产生的验证组件。一系列简单的例子展示了我们的工作方法。
2021-09-20 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 formally verified proof of the Central Limit Theorem
我们描述了一个证明的中心极限定理，已正式核实的伊莎贝尔证明助手。我们的形式化的基础上，并扩展伊莎贝尔的图书馆分析和测量理论的概率。该定理的证明使用特征函数，这是一种傅立叶变换，以证明，在适当的假设下，随机变量的总和弱收敛到标准正态分布。我们还讨论了支持正式化的库和基础设施，并反思了我们从这一努力中吸取的一些教训。
2017-02-01 cs.LO cs.MS math.PR
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 Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle
一个伊莎贝尔/HOL形式化哥德尔的两个不完全定理。这项工作遵循Zeriwierczkowski的详细证明定理使用遗传有限（HF）集理论。避免通常的算术编码的语法消除了形式化的必要性，在嵌入式逻辑演算的初等数论。伊莎贝尔形式化使用两个单独的治疗变量绑定：标称包的规模，以发展这种复杂性，而德Bruijn指数原来是理想的编码语法。伊莎贝尔证明的关键细节进行了描述，特别是在文献中发现的差距和错误。
2021-04-28 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
Homotopy Type Theory in Isabelle
本文介绍了Isabelle/HoTT，同伦类型论的第一个发展Isabelle证明助手。在Paulson早期工作的基础上，我使用Isabelle现有的逻辑框架基础设施来实现基本的自动化，例如类型检查和术语细化，这通常是在依赖类型系统的源代码级别上处理的。我还集成了命题作为类型的范式与声明性的Isar证明语言，提供了一种替代的Coq和Agda的证明条款的基于策略的证明。基础设施开发，然后用于形式化的同伦类型论书的基础结果。
2021-04-19 cs.LO
The Foundation of a Generic Theorem Prover
Isabelle是一个交互式定理证明器，支持各种逻辑。它将规则表示为命题（而不是函数），并通过组合规则来构建证明。这些操作构成了一个元逻辑（或“逻辑框架”），其中对象逻辑被形式化。伊莎贝尔现在是基于高阶逻辑-一个精确和良好理解的基础。示例说明了使用此元逻辑来形式化逻辑和证明。一阶逻辑的公理被证明是可靠和完备的。后向证明通过关于对象级蕴涵的元推理形式化。高阶逻辑比其他元逻辑有几个实际的优势。许多证明技术是已知的，如休特的高阶统一程序。
2000-10-31 cs.LO
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL
我们提出了一个证明过程中的Isabelle/HOL的一元实多项式问题。我们的过程的核心数学是基于单变量柱形代数分解。我们遵循不可信证书的方法，将解决与验证分离：高效的外部工具执行昂贵的真实代数计算，产生在Isabelle逻辑中正式检查的证据。这使我们能够利用高度调整的计算机代数系统，如Mathematica来指导我们的过程，而不会影响其结果的正确性。我们目前的实验证明这种方法的有效性，在许多情况下产生的数量级的改进，比以前的方法。
2018-04-10 cs.LO
Teaching a Formalized Logical Calculus
经典一阶逻辑在许多方面都是数学、语言学、计算机科学和人工智能的核心，因此有必要详细定义它。我们提出了合理性和完整性证明的一阶逻辑，形式化的互动证明助手伊莎贝尔/HOL的一个微积分。我们的形式化是基于Stefan Berghmann的工作，我们已经更新为使用Isabelle的声明式证明风格Isar（正式证明档案，条目FOL-Fitting，2007年8月/2018年7月）。我们用de Bruijn指数表示变量;这使得在量词下的替换对人类读者来说不那么直观。然而，与使用字符串表示的变量的替换实现相比，自然数的性质产生了一个优雅的解决方案。所考虑的微积分具有一个总是空的前件和一个在后件中的公式列表的特殊性质。我们得到的可靠性和完整性的证明，作为其tableau对应的逆对偶的派生结果的微积分。我们努力不仅提出的结果的合理性和完整性的证明，但也提供了一个深入到一个类似编程的方法，一阶逻辑语法，语义和微积分的形式化。我们在一门计算机科学专业的逻辑本科课程中使用了这种形式化，并讨论了我们的经验。
2020-02-28 cs.LO
Evaluating Automatic Difficulty Estimation of Logic Formalization Exercises
有效地教授逻辑需要理解导致逻辑学生挣扎的因素。形式化练习要求学生产生与自然语言句子相对应的公式，这是一个很好的审查候选人，因为它们挖掘了学生对逻辑各个方面的理解。我们将先前提出的难度估计算法预测的形式化练习的难度与Grade Grinder语料库上的两个经验难度措施相关联，Grade Grinder语料库包含FOL练习的学生解决方案。我们得到一个适度的相关性与这两个措施，这表明该算法确实利用到重要的困难来源，但留下了相当数量的方差未捕获。我们进行错误分析，仔细检查被错误分类的练习，目的是确定其他困难的来源。我们确定了三个额外的因素，出现从难度分析，即谓词复杂性，语用因素和典型的练习，并讨论了自动化的难度估计逻辑教学和可解释的人工智能的影响。
2022-04-26 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
Formalization of Fault Trees in Higher-order Logic: A Deep Embedding Approach
故障树（FT）是一种标准的故障建模技术，已被广泛用于预测许多复杂工程系统的可靠性，可用性和安全性。为了便于形式化分析FT的分析，最近提出了一种高阶逻辑形式化的FT。然而，这种形式化在处理大型系统和将FT模型转换成其相应的可靠性框图（RBD）结构方面是相当有限的，即，在可靠性和可用性分析中经常使用的转换。为了克服这些限制，我们提出了一个基于深度嵌入的形式化的FT。特别地，本文提出了AND、OR和NOT FT门的形式化，这些FT门又用于形式化其他常用的FT门，即，与非、或非、异或、抑制、比较器和多数表决等方法，并对其失效概率表达式进行了形式化验证。为了说明的目的，我们提出了一个正式的故障分析的通信网关软件的下一代空中交通管理系统。
2016-08-23 cs.LO
Formalizing Determinacy of Concurrent Revisions
并发修订是一种并发控制模型，旨在保证确定性，这意味着程序的结果是唯一确定的。本文描述了一个Isabelle/HOL形式化的模型的操作语义和证明的确定性。我们讨论并解决了操作语义中微妙的歧义，并简化了确定性的证明。虽然我们的研究结果并没有出现相应的实现中的错误，形式化突出了并发控制模型的设计和验证所涉及的一些挑战。
2019-12-20 cs.LO
Formalization of Complex Vectors in Higher-Order Logic
复向量分析在物理学和工程学等许多学科中被广泛用于分析连续系统。在本文中，我们提出了一个高阶逻辑形式化的复向量空间，以方便进行这种分析的声音的核心定理证明：HOL光。我们对复向量的定义建立在复数和实向量的定义之上。这种扩展使我们能够广泛地受益于已经验证的定理的基础上复杂的分析和真正的向量分析。为了显示我们的图书馆的实用性，我们采用它来形式化电磁场，并证明了平面波的反射定律。
2014-05-15 cs.LO
Towards a Coq formalization of a quantified modal logic
本研究在Coq证明助手中实现了单模态量化反思演算$\textsf{QRC}_1$的深度嵌入，完成可变论域Kripke模型与可靠性定理的形式化，梳理设计决策并给出简化的新证明。
2022-07-02 cs.LO
Towards the Formalization of Fractional Calculus in Higher-Order Logic
分数阶微积分是将经典的积分和微分理论推广到任意阶（即，实数或复数）。在过去的二十年里，这种新的数学建模方法已被广泛用于分析各种科学和工程领域的广泛的物理系统。在本文中，我们描述了一个正在进行的项目，旨在形式化的分数阶微积分的基本理论的HOL光定理证明。主要是，我们提出了这种形式化工作的动机和应用，实现我们目标的路线图，项目的当前状态和未来的里程碑。
2015-05-08 cs.LO
Formalization of PAL$\cdot$S5 in Proof Assistant
作为证明助手在逻辑研究中应用的一个尝试，我们在Lean定理证明器中使用PAL风格的动态模态形式化了多主体模态逻辑S5的模型和证明系统。我们对公告的归约公理以及模态逻辑S5的可靠性和完备性提供了形式化的证明，可以用Lean 3.19.0进行类型检查。完整的证明现在可以在Github上找到。
2020-12-17 cs.LO
On Exams with the Isabelle Proof Assistant
Technical University of Denmark（丹麦技术大学）
我们提出了一种方法来测试学生的学习成果，在自动推理的过程中使用伊莎贝尔证明助手。该方法使我们能够测试一般理解的形式证明在各种逻辑证明系统和理解的证明，特别是在高阶逻辑的伊莎贝尔/HOL。使用Isabelle几乎可以自动对考试的大部分内容进行评分。我们通过一些示例问题来解释我们的方法，并解释为什么我们认为我们选择的每种问题都足以衡量我们预期的学习成果。最后，我们讨论了我们的经验，使用的方法考试的课程自动推理，并建议潜在的未来工作。
2023-03-10 cs.AI cs.LO
