A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
我们提出了一个综合的两个证明风格的交互式定理证明：程序风格（其中证明是脚本的命令，如在Coq）和声明式风格（其中证明是文本在一个受控的自然语言，如在Isabelle/Isar）。我们的方法结合了声明式风格的优点-编写正式证明的可能性，如正常的数学文本-和程序风格-强大的自动化和帮助形成的证明，包括确定中间步骤的声明。我们的方法是新的，显着不同的方式，程序和声明式的证明风格已经结合在伊莎贝尔，Ssreflect和Matita系统。我们的方法是通用的，可以实现任何程序的交互式定理证明器，无论其架构和逻辑基础。为了展示我们提出的方法的可行性，我们将其完全实现为一个名为miz 3的证明接口，位于HOL Light交互式定理证明器之上。这个接口使用的声明式语言是Mizar系统语言的一个轻微变体，可以用于任何交互式定理证明器，无论其逻辑基础如何。miz 3界面允许轻松访问HOL Light的全套战术和正式库，因此具有“工业实力”。我们的方法提供了一种方法，自动转换任何程序的证明，一个声明的副本，其中转换后的证明是类似的大小，原来的。由于所有的声明式系统本质上都有相同的证明语言，这提供了一种在交互式定理证明器之间移植证明的简单方法。
2012-03-27 cs.LO
Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers
School of Software, Northwestern Polytechnical University（西北工业大学软件学院）；School of Computer Science and Ningbo Institute, Northwestern Polytechnical University（西北工业大学计算机科学与宁波研究院）；Research Institute of Trustworthy Autonomous Systems, Southern University of Science and Technology（南方科技大学可信自主系统研究院）；Department of Computer Science and Engineering, Southern University of Science and Technology（南方科技大学计算机科学系）
本文研究了现有证明合成技术无法证明的定理特征，提出基于人类专家证明模式的模式引导战术搜索方法，提升证明成功率和复杂定理的证明能力。
2026-04-27 cs.LO
Interactive Visualization of Saturation Attempts in Vampire
形式化方法的许多应用需要对系统属性进行自动推理，例如系统安全性和保密性。为了提高自动推理引擎（如SAT/SMT求解器和一阶定理证明器）的性能，有必要了解这些引擎在生成正式证书（如逻辑证明和/或模型）方面的成功尝试和失败尝试。这种分析是具有挑战性的，因为在证明/模型搜索期间生成了大量的逻辑公式。在本文中，我们专注于饱和为基础的一阶定理证明，并介绍了SATVIS工具的交互式可视化饱和为基础的证明尝试在一阶定理证明。我们建立在世界领先的定理证明器VAMPIRE之上的SATVIS，通过交互式可视化SATVIS中VAMPIRE的饱和尝试。我们的工作结合了自动布局和可视化的衍生图引起的饱和尝试与交互式转换和搜索功能。因此，我们能够分析和调试（失败）证明尝试的吸血鬼。由于其交互式可视化，我们相信SATVIS可以帮助专家和非专家在定理证明理解一阶证明和分析/完善失败的证明尝试的一阶证明。
2020-01-13 cs.LO
LogicProof: An Interactive Web-Based Educational Theorem Prover for Natural Deduction and Sequent Calculus across Classical and Constructive Logics
Technical University of Košice（科希策理工大学）
介绍LogicProof这一用于教育的交互式网络定理证明器，支持经典和构造性逻辑的自然演绎与相继式演算，经学生测试能提升对形式证明构建的理解，补充现有教学方法。
2026-07-07 cs.LO
Interactive Proof Presentations with Cobra
我们提出了眼镜蛇，一个现代的证明演示框架，利用尖端的演示技术与最先进的交互式定理证明器一起，将形式化的数学作为活动文档呈现。眼镜蛇提供了一种简单的方式来提出证明和一种新颖的方法，礼堂互动。演示文稿由定理证明者现场检查，并且允许演示者和观众进行现场更改。
2017-01-25 cs.LO
Abstraction boundaries and spec driven development in pure mathematics
本文探讨纯数学研究中如何借助交互式定理证明器强化抽象边界与规格驱动开发，从而管理复杂性，并论证其相较传统隐式实践的额外质性优势。
2023-09-26 cs.CY cs.LO math.AG
An interactive semantics of logic programming
我们适用于逻辑编程的一些最近出现的想法，从该领域的减少为基础的通信系统，目的是提供证据的隐藏的相互作用和协调机制，规则的运作机制，这样的编程范式。语义框架，我们选择了我们的结果是瓦片逻辑，它的优点是允许一个统一的治疗目标和意见，并应用抽象的分类工具来证明结果。作为主要的贡献，我们提到的有限表示的抽象统一，和并发和协调的抽象语义逻辑编程的最常见的语义相一致。此外，拼块语义的组合性由标准结果保证，因为它减少了对与逻辑程序相关联的拼块系统享有拼块分解属性的检查。还讨论了处理约束系统的方法的扩展。
2001-07-17 cs.LO cs.PL
Resource Adaptive Agents in Interactive Theorem Proving
Universität des Saarlandes（萨尔大学）
本文提出了一种支持用户进行交互式定理证明的资源自适应代理机制。该机制使用两层体系结构的代理社会建议适当的命令连同可能的命令参数实例化。实验结果表明，通过引入资源概念，该方法的有效性可以得到进一步提高。在本文中，我们提供了一个抽象的整体机制，激励适当的资源概念的必要性，并讨论其实现的代理体系结构。
2009-01-23 cs.AI cs.LO
ProofPeer - A Cloud-based Interactive Theorem Proving System
ProofPeer致力于成为一个基于云的交互式定理证明系统。在说明了为什么需要这样一个系统之后，本文提出了ProofPeer要取得成功需要满足的一些设计挑战。上下文作为一个解决方案的ProofPeer的用户之间共享证明状态的问题。编年史是作为一种组织和版本上下文的方式引入的。
2012-01-02 cs.DL cs.LO cs.MS
How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers
近年来，交互式定理证明器的有效性已经增加到一定程度，使得交互过程中的瓶颈转移到效率上：虽然原则上大型和复杂的定理是可证明的（有效性），但用户与系统交互需要花费大量精力（缺乏效率）。我们进行了焦点小组，以评估Isabelle/HOL和键系统的可用性有两个目标：（a）检测交互式定理证明者和他们的用户之间的交互的可用性问题，（b）分析如何评价和调查方法常用的人机交互，如焦点小组和合作评估，适用于特定领域的交互式定理证明（ITP）。在本文中，我们报告我们的经验，使用评估方法焦点小组，以及我们如何适应这种方法，ITP。我们主要在“元水平”上描述我们的结果和结论，即，我们专注于ITP的具体特征对焦点小组的设置和结果的影响。在具体层面上，我们简要总结了我们的案例研究中使用的ITP的可用性的见解。
2014-10-30 cs.HC cs.LO
A Resolution-Based Interactive Proof System for UNSAT
Technical University of Munich（慕尼黑工业大学）
本文通过将交互式证明系统与消解过程结合，提出了首个针对Davis-Putnam消解过程的交互协议，并证明了寻找竞争性交互协议可归结为寻找满足交换性质的公式算术化问题。
2026-05-21 cs.LO
Topological Interpretation of Interactive Computation
University of Camerino（卡梅里诺大学）；Stony Brook University（石溪大学）
我很高兴写这篇文章来纪念斯科特·A。斯莫尔卡65岁生日。我们重新审视Goldin，Smolka假设，即持久图灵机（PTM）可以捕获顺序交互计算的直观概念.我们提出了一个拓扑设置模型的抽象概念的环境。我们用它来定义一个拓扑图灵机（TTM）的概念，作为一个通用的模型，交互式计算和并发计算的可能模型。
2019-08-03 cs.AI cs.LO
Beginners' Quest to Formalize Mathematics: A Feasibility Study in Isabelle
使用交互式定理证明器有多难？我们的回应，审查形式化的希尔伯特的第十个问题在伊莎贝尔/HOL进行的本科生研究小组在雅各布斯大学不来梅。我们认为，我们的例子表明，证明助手是可行的初学者形式化数学。为了使该领域更容易访问，我们还调查了学习交互式定理证明器时出现的障碍。从广义上讲，我们主张在数学研究和课程中更多地采用交互式定理证明器。
2021-06-23 cs.LO
Persistent Queries
我们提出了一个语法和语义的交互式抽象状态机来处理以下情况。在某个步骤期间发出查询，但该步骤在收到任何答复之前结束。稍后，一个回复到达，然后算法使用这个回复。持久查询是指可能使用延迟回复的查询。从语法上讲，我们的建议包括发出一个持久查询，以及一个存储延迟回复的位置。在语义上，它只涉及对现有的交互式小步抽象状态机理论的微小修改。
2008-11-05 cs.LO cs.PL
An abstract fixed-point theorem for Horn formula equations
针对计算机科学多应用中重要的Horn公式方程，本文在带最小不动点算子的一阶逻辑中证明了适用于抽象语义的抽象不动点定理，并阐述其在程序验证逻辑基础等计算逻辑领域的推论。
2025-11-11 cs.LO math.LO
The Abella Interactive Theorem Prover (System Description)
Abella是一个交互式系统，用于推理对象语言的各个方面，这些方面已经通过基于语法结构的递归规则正式呈现。Abella使用两级逻辑方法来规范和推理。一个级别由规范逻辑定义，该规范逻辑支持结构语义规则的透明编码，并且还支持它们的执行。第二个层次，称为推理逻辑，嵌入规范逻辑，并允许开发有关规范的属性的证明。这两种逻辑的一个重要特征是，它们利用lambda树语法方法来处理对象语言中的绑定。除此之外，Abella还被用来证明λ演算的正规化性质、λ演算的截容许性、类型唯一性和主体归约性质。本文讨论了Abella的逻辑基础，概述了它支持的定理证明的风格，最后描述了它最近的一些应用。
2008-05-23 cs.LO cs.PL
Integrating Testing and Interactive Theorem Proving
Northeastern University（东北大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）
使用交互式定理证明器来推理程序涉及一系列交互，其中用户用图解来挑战定理证明器。然而，许多提出的证明实际上是错误的，用户在意识到这一点之前经常花费相当大的精力来检查定理证明器的输出。我们提出了一个协同集成的测试与定理证明，实现在ACL2轿车（ACL2），自动生成具体的反例。我们的方法使用的全部权力的定理证明和相关的库来简化代数，这种简化可以转换代数，找到反例是很难的代数，找到反例是平凡的。事实上，我们的方法甚至会导致更好的定理证明，例如，如果测试表明推广步骤导致错误的猜想，我们会迫使定理证明器回溯，允许它追求更富有成效的选择，可能会产生证明。本文的重点是工程的协同集成测试与交互式定理证明，这包括扩展ACL 2的新功能，我们希望是普遍感兴趣的。我们还讨论了我们的经验，在使用ACL2教新生如何对他们的程序的原因。
2011-10-21 cs.AI cs.LO cs.SE
Intensional Kleene and Rice Theorems for Abstract Program Semantics
可计算性理论中的经典结果，特别是赖斯定理，集中于程序的扩展内容，即程序计算的部分递归函数。后来和最近的工作调查了这些结果的内涵概括，这些结果考虑到函数计算的方式，从而受到计算它们的特定程序的影响。在本文中，我们挑出一类新的程序语义的基础上抽象域的程序属性，能够捕捉非扩展方面的程序计算，如其渐近复杂性或逻辑不变，并允许我们概括一些基本的可计算性结果，如赖斯定理和Kleene的第二递归定理，这些语义。特别是，事实证明，对于这一类的抽象程序语义，任何非平凡的抽象属性是不可判定的，每一个可判定的过度近似必然包括一个无限的假阳性集，涵盖了语义抽象域的所有值。
2021-09-14 cs.FL cs.LO
A Macro for Reusing Abstract Functions and Theorems
尽管ACL 2逻辑是一阶的，但ACL 2系统提供了几种机制，为用户提供类似于高阶逻辑的操作。在本文中，我们提出了一个宏，命名为instance-of-defspec，以方便重用的抽象函数和事实证明他们。Defspec是一本ACL 2书籍，允许用户定义约束函数及其相关属性。它包含了便于定义这种抽象规范及其实例的宏。目前，从这些抽象函数导出的引理和定理不会自动实例化。这正是我们新宏的目的。instance-of-defspec将不仅实例化规范内的函数和定理，而且实例化在规范之上构建的更多函数和定理。作为一个工作示例，我们描述了monoid上的各种折叠函数，这些函数是我们从任意函数逐渐构建的。
2013-04-30 cs.LO cs.PL
An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support
基于不变式的编程（IBP）是一种基于结构的正确的编程方法，其中程序是围绕不变式构建的，这些不变式在实际代码之前被另外制定。Socos是一个专门为支持IBP而构建的程序构建和验证环境。Socos的前端是一个图形化的图表编辑器，允许程序员构建基于不变式的程序并检查其正确性。Socos的后端组件，程序检查器，计算程序的验证条件，并试图自动证明它们。它使用定理证明器PVS和SMT求解器Yices来尽可能多地释放验证条件，而无需用户交互。在本文中，我们首先从用户和系统级的角度描述了Socos环境，然后通过在Socos中构建一个经过验证的堆排序实现来验证IBP工作流。案例研究突出了自动和交互式定理证明在IBP工作流程的三个连续阶段的作用：开发的背景理论，制定程序规范和不变量，并证明最终实现的正确性。
2012-02-22 cs.LO cs.PL
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
Australian National University（澳大利亚国立大学）；Defence Science and Technology Group（国防科学技术集团）；BIMLOGIQ；Google DeepMind（谷歌DeepMind）
针对交互式定理证明（ITP）研究分散、方法难比较的问题，提出BAIT框架，通过比较公式嵌入的先进架构、评估端到端证明性能，为ITP学习方法提供公平简化的比较基准，助力未来研究。
2024-03-06 cs.AI cs.LG cs.LO
Common Denominator for Value and Expectation No-go Theorems: Extended Abstract
隐变量（HV）理论声称量子态描述了由隐变量值区分的系统系综。不可行定理断言HV理论不能与量子理论的预言相匹配。目前的工作开始修复文献中的缺陷不去定理断言，HV理论不能预测的期望值的测量。该文献给人的印象是，期望不去定理推翻了历史悠久的不去定理，声称HV理论不能预测可能的测量值。但这两种方法涉及不同类型的测量。这就妨碍了它们之间的相互比较。只有投影测量是两者共有的。在这里，我们锐化这两种方法的结果，以便只使用投影测量。这使我们能够澄清这两种方法之间的相似性和差异。两者都不占主导地位。
2018-03-02 cs.LO quant-ph
Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers
Heriot-Watt University（赫瑞-瓦特大学）；University of Strathclyde（思克莱德大学）；University of Edinburgh（爱丁堡大学）
神经网络的验证是当前自动定理证明中的一个热点问题。进展非常迅速，现在有各种各样的工具可以验证具有数十万个节点的网络的属性。从理论上讲，这为验证使用神经网络组件的大型控制系统打开了大门。然而，虽然工作已经成功地将这些验证的结果，以证明个别系统的更大的属性，目前还没有通用的方法来弥合验证和交互式定理证明（ITP）之间的差距。在本文中，我们提出了车辆，我们的解决方案，这个问题。车辆配备了一个表达领域特定的语言，用于说明神经网络规范，可以编译为验证器和ITP。它通过使用标准ONNX文件作为网络的单一规范表示，克服了以前类似ITP形式化中的可维护性和可扩展性问题。我们证明了它的实用性，使用它连接神经网络验证器Marabou到Agda，然后正式验证由神经网络驾驶的汽车永远不会离开道路，即使面对不可预测的侧风和不完美的传感器。该网络具有超过20，000个节点，因此该证明比关于ITP中的神经网络增强系统的先前证明提高了3个数量级。
2022-02-10 cs.LG cs.LO cs.PL
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
University of Innsbruck（因斯布鲁克大学）；Czech Academy of Sciences（捷克科学院）；University of Melbourne（墨尔本大学）
本研究将交互式定理证明中的策略预测建模为归纳逻辑编程任务，通过丰富特征空间学习可解释规则，并用于过滤现有策略选择方法，实验证明能提升性能。
2024-11-02 cs.AI cs.LG cs.LO
