Interpolation with Automated First-Order Reasoning
University of Potsdam（波茨坦大学）
从一阶逻辑全自动定理证明角度研究插值法，介绍克雷格插值的两阶段方法及获取基础插值的方式，提及等式编码等贡献，还引入二阶量词消除作为统一插值方法并描述相关算法。
2026-07-08 cs.LO
The Cross-Domain State Preservation Functor: A Mechanized Theory of Regulatory State Synchronization in Isabelle/HOL
Oraclizer Labs（Oraclizer实验室）；Oraclizer Labs Korea（Oraclizer韩国实验室）
本文通过Isabelle/HOL中的机械化证明，建立了跨域状态同步系统在拜占庭故障下的安全性和活性，包括状态保存的忠实反映和冲突解决的确定性。
2026-08-25 cs.CR cs.LO
A Concurrent Program Logic with a Future and History
细粒度的乐观并发程序仍然是一个悬而未决的问题。现代程序逻辑提供了抽象机制和组合推理原则来处理固有的复杂性。然而，它们的使用主要局限于纸张和纸张或机械化的证明。我们设计了一个新的分离逻辑，面向缺乏自动化。虽然本地推理是众所周知的自动化是至关重要的，我们是第一个展示如何保持这种局部性（i）推理归纳属性，而不需要幽灵代码，和（ii）推理计算历史的事后诸葛亮。我们在一个工具中实现了我们的新逻辑，并使用它来自动验证具有挑战性的并发搜索结构，这些结构需要归纳属性和事后推理，例如Harris集。
2022-11-11 cs.LO cs.PL
Adelfa: A System for Reasoning about LF Specifications
我们提出了一个系统，称为Adelfa的爱丁堡逻辑框架或LF开发的规格推理提供机械化的支持。Adelfa的基础是一个新的逻辑，名为L_LF。LF中的类型判断由L_LF中的原子公式表示，并且允许对出现在这样的公式中的上下文和术语进行量化。上下文，这构成了类型分配给唯一命名的变量，使用名义常数的技术设备建模，在L_LF的特点是上下文模式，描述其归纳结构。我们提出了这些公式和相关的语义之前，勾勒出一个证明系统，用于构建参数，是健全的语义。然后，我们概述了这个证明系统在Adelfa中的实现，并通过几个示例证明的发展来说明它的使用。最后，我们将Adelfa与现有的LF规范推理系统联系起来。
2021-07-16 cs.LO cs.PL
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
本文提出ReLoC Reloaded，一种基于Iris框架的机械化关系分离逻辑，用于证明高阶状态与细粒度并发程序的精化关系，并扩展了逻辑原子关系规范，支持预言变量以增强实用性。
2021-07-20 cs.LO cs.PL
HistMSO: A Logic for Reasoning about Consistency Models with MONA
Institut Polytechnique de Paris（巴黎理工学院）；Université Côte d’Azur, CNRS, I3S（蔚蓝海岸大学，法国国家科学研究中心，I3S研究所）
本文提出HistMSO逻辑，用于推理复制数据系统的一致性模型，展示了其能表达42种一致性模型中的39种，并利用MONA工具进行自动推理。
2026-04-03 cs.DC cs.FL cs.LO
Mechanizing Coinduction and Corecursion in Higher-order Logic
递归和上递归定义的理论已经在高阶逻辑（HOL）中得到了发展，并使用Isabelle进行了机械化。最小不动点表示归纳数据类型，如严格列表;最大不动点表示共归纳数据类型，如懒惰列表。良基递归表示归纳数据类型上的递归函数;协递归表示产生共归纳数据类型元素的函数。该理论依赖于传统的形式化的无限树。该理论旨在用于规范和验证。它支持大范围的可计算函数的推理，但没有形式化它们的操作语义，也可以表示不可计算函数。该理论说明使用有限和无限的列表。共递归表示无限列表上的函数;共归纳推理这类函数。
2000-10-31 cs.LO
A Separation Logic for Concurrent Randomized Programs
我们提出了北极星，支持概率推理的并发分离逻辑。作为我们的逻辑的一部分，我们扩展了耦合的想法，这是最近的工作概率关系逻辑的基础，设置的程序与概率和非确定性的选择。为了演示北极星，我们验证了一个随机并发计数器算法和两级并发跳表的变体。我们所有的结果都在Coq中实现了机械化。
2018-11-21 cs.LO cs.PL
Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
Southwest University（西南大学）；State Key Laboratory of Intelligent Vehicle Safety Technology（智能车辆安全全国重点实验室）；Aarhus University（奥胡斯大学）；University of York（约克大学）
本文在Isabelle/HOL中形式化分析了Sigmoid函数并证明了通用逼近定理，填补了形式化证明库的空白，提升了神经网络的可信度。
2025-12-03 cs.LO cs.SE
Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs
Aarhus University（奥胡斯大学）；New York University（纽约大学）
研究对抗性概率程序，提出埃尔顿这一高阶分离逻辑，利用语言层面延迟采样和逻辑层面瓮资源等工具，结合其他特性，能证明安全示例错误界限，且证明已机械化验证。
2026-07-16 cs.LO cs.PL
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
提出Coneris，首个高阶并发分离逻辑，通过随机逻辑原子性支持并发概率程序的错误概率界模块化推理，并在Rocq和Iris中机械化验证。
2025-08-07 cs.LO cs.PL
Are Dependent Types in Set Theory Feasible?
EPFL（洛桑联邦理工学院）；KTH Royal Institute of Technology（瑞典皇家理工学院）
本文提出在集合论中机械嵌入依赖函数类型的方法，通过Lisa证明助手实现，并展示如何利用集合论公理进行依赖类型的自动推理。
2026-03-13 cs.LO
A Theorem Prover for Quantum Hoare Logic and Its Applications
量子霍尔逻辑（QHL）在Ying的工作中被引入来描述和推理量子程序。在本文中，我们实现了一个定理证明QHL基于Isabelle/HOL。通过应用定理证明器，验证一个量子程序的规格等价地转化为矩阵之间的顺序关系。由于Isabelle/HOL的局限性，顺序关系的计算通过调用外部Python语言的oracle来解决。据我们所知，这是量子程序的第一个定理证明器。为了证明它的力量，两个著名的量子算法，即，Grover量子搜索和量子相位估计是Shor的多项式时间分解量子算法的关键步骤，利用定理证明器证明了这两个步骤。这是他们两人的第一次机械化证明。
2016-01-15 cs.LO
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
Aarhus University（奥胡斯大学）；New York University（纽约大学）；Amazon Web Services（亚马逊云科技）
本文提出Foxtrot，首个用于证明高阶并发概率程序上下文细化的高阶分离逻辑，结合了并发推理原理与概率推理原理，展示了其在对抗性von Neumann硬币和Sodium加密库中的应用。
2026-04-27 cs.LO cs.PL
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
针对现有方法无法为高阶概率程序提供精确误差界的问题，本文提出含“错误信用”资源的高阶分离逻辑Eris，支持新推理原则，能证明哈希碰撞等场景的摊销误差界及拒绝采样算法的正确性，且结果已机械化验证。
2024-11-29 cs.LO cs.PL
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
高阶并发语言的更精确的正确性证明是困难的：它们涉及到在并发的高级源语言和使用低级共享内存原语的实现之间建立一个保持终止的精化。然而，现有的逻辑证明并发加细要么忽略属性，如终止，或只处理一阶状态。在本文中，我们解决这些限制，扩展虹膜，最近的高阶并发分离逻辑，支持终止保留的细化推理。为了证明这些扩展的功能，我们证明了一个高阶，会话类型的语言的有效实现的正确性。据我们所知，这是第一个能够为这种语言提供编译器正确性证明的程序逻辑。我们的扩展和我们的编译器正确性证明的合理性已经在Coq中机械化。
2017-01-20 cs.LO cs.PL
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
本文提出高阶近似关系分离逻辑 Approxis，通过误差信用支持概率高阶有状态程序的近似与精确等价推理，并在 Coq/Iris 中机械化验证安全与采样示例。
2024-12-03 cs.LO cs.PL
Reasoning about Weak Isolation Levels in Separation Logic
本文针对工业级数据库默认弱隔离级别存在隔离性错误但缺乏可执行实现推理模型的问题，在分离逻辑中形式化读未提交、读已提交和快照隔离三个弱隔离级别，验证其规范可禁止违规执行、可实现且存在蕴含关系。
2025-08-20 cs.LO cs.PL
A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems
本文提出了一种基于算法的方法来证明命题系统的归纳性质，如可容许性，可逆性，割消和单位扩展。虽然一般来说是不可判定的，但这些结构属性在证明理论中是至关重要的，因为它们可以减少证明搜索工作，并进一步用作获得其他元结果（如一致性）的脚手架。算法-利用重写逻辑元逻辑框架，并使用重写和缩小为基础的推理-详细解释，并说明整个文件的例子。他们已经完全机械化的L-框架，从而提供了一个正式的规约语言和现成的机械化的证明搜索算法来证明定理和元定理的目标系统的半决策程序。本文通过实例分析说明，L-框架在单结论和多结论直觉逻辑、经典逻辑、经典线性逻辑及其二元系统、直觉线性逻辑和正规模态逻辑等命题推理系统上的应用，实现了很大程度的自动化。
2021-01-08 cs.LO math.LO
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
本文提出高阶分离逻辑Tachis，通过引入概率成本信用资源来推理概率程序的期望成本，支持摊还分析与多种成本模型，并经Coq等工具机械化验证了多种算法的期望成本上限。
2024-11-12 cs.LO cs.PL
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
本文针对依赖类型高阶逻辑DHOL提出原生表推演自动推理规则，并在Lash中实现，借助DHOL到HOL的可靠完备翻译保证完备性，实验表明其性能优于在翻译结果上运行的主流HOL证明器。
2024-10-18 cs.LO
Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL
信息物理和机器人系统的形式化验证要求我们能够准确地对现实世界中存在的物理量进行建模。在这些量中使用显式单位可以允许更高程度的严格性，因为我们可以确保计算中量的兼容性。同时，单位的不当使用可能是安全的障碍，因此非常希望在物理计算中进行自动化的健全性检查。在本文中，我们贡献了一个机械化的国际单位制（ISQ）和相关的国际单位制在伊莎贝尔/HOL。我们展示了如何伊莎贝尔可以用来提供一个类型系统的物理量，和自动化的证明支持。向量由对应于基向量的维度类型参数化，因此只有相同维度的量才能相等。由于基本的“量的代数”诱导的数量和SI类型的一致性，具体的战术支持开发，以捕捉这些。我们的建设验证了一个测试集的数量和SI单位之间的已知等价。此外，所提出的理论可以用于SI系统和其他系统（如英国帝国系统（BIS））之间的类型安全转换。
2023-02-15 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
Two Results on Separation Logic With Theory Reasoning
本文给出了关于谓词符号为归纳定义的分离逻辑和理论推理中蕴涵问题的两个结果。首先，我们证明了在理论推理的情况下，对于树宽有界的规则，蕴涵问题是不可判定的。这一结果适用于许多理论，即使它们的表达能力很低。例如，它适用于具有后继函数或具有通常顺序的自然数。其次，我们证明了每个蕴涵问题都可以归结为一个蕴涵问题，不包含平等（无论是在公式中，也不是在递归规则定义的谓词符号的语义）。
2022-06-19 cs.LO
Object-Level Reasoning with Logics Encoded in HOL Light
我们提出了一个通用的框架，有利于对象级推理与逻辑编码的高阶逻辑定理证明环境HOL光。这涉及到在任何逻辑中使用直观的前向和后向链接以微积分风格证明语句。它是由自动化的机器，照顾必要的结构推理和自动匹配的术语。我们的框架还可以处理类型理论的对应证明，有效地允许类型检查和建设的计算过程通过证明。我们演示了我们的实现使用一个简单的命题逻辑和Curry-Howard对应的Alzada演算，并认为它的使用与线性逻辑和它的各种对应的会话类型。
2021-01-11 cs.LO cs.SC
First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation
MPI-SWS（马克斯·普朗克软件系统研究所）；Saarland University（萨尔兰大学）；CISPA Helmholtz Center for Information Security（CISPA赫尔霍夫信息安全中心）；University of Konstanz（康斯坦茨大学）
本文提出Amaryllis，首个支持独立性和条件推理并处理动态内存分配的概率通用逻辑，通过新的索引估值模型和Iris核心概念的适应，实现了概率推理和动态分配的验证。
2026-08-03 cs.LO cs.PL
First Experiments with a Flexible Infrastructure for Normative Reasoning
Computer Science and Communications, University of Luxembourg（卢森堡大学计算机科学与通信学院）
一个灵活的基础设施规范推理概述。一个小规模的演示版本的设想系统已实施的证明助手伊莎贝尔/HOL利用第一作者的通用逻辑推理方法的基础上浅语义嵌入元逻辑HOL。这样一个灵活的推理基础设施的需要是有动机的，并说明了从一般数据保护条例中选择的一个相反的职责的示例方案。
2018-04-09 cs.AI cs.LO
Interpolation Theorems for Nonmonotonic Reasoning Systems
克雷格插值定理（Craig's interpolation theorem，Craig 1957）是命题逻辑和一阶逻辑中的一个重要定理。它说，如果一个逻辑公式$β$在逻辑上从一个公式$α$得出，那么就有一个公式$γ$，只包括出现在两个$α,β$中的符号，这样$β$在逻辑上从$γ$得出，而$γ$在逻辑上从$α$得出。这样的定理对于理解它们所处的逻辑以及加速用这些逻辑中的理论进行推理是重要和有用的。在本文中，我们提出了插值定理在这种精神的三个非单调系统：限制，默认逻辑和逻辑程序的稳定模型语义（a.k.a.）。答案集语义）。这些结果使我们更好地理解这些逻辑，特别是与它们的非单调特性相比。他们认为，一些\emph{monotonicity}原则持有，尽管这些逻辑的经典单调性失败。此外，它们有时允许我们使用这些系统的推理分解方法，可能会增加它们的适用性和易处理性。最后，它们允许我们构建使用这些逻辑的结构化表示。
2002-07-16 cs.AI cs.LO
Normative Conditional Reasoning as a Fragment of HOL
本文通过Isabelle/HOL浅层语义嵌入机械化Aqvist条件义务系统E，既用于自动验证道义对应关系，也用于编码Parfit令人反感的结论，提出弱化传递性而非完全放弃的替代方案。
2024-07-07 cs.AI cs.LO cs.SC
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
Quantitative Logic Reasoning
University of São Paulo（圣保罗大学）
在本文中，我们展示了同时处理演绎和定量推理的逻辑系统之间的几个相似之处。我们认为把这些系统执行的任务称为定量逻辑推理是合适的。类似的性质保持整个类，其成员存在一套线性代数技术适用于研究可满足性决策问题。在这个演示中，我们认为定量逻辑推理的任务所执行的命题概率逻辑;一阶逻辑计数量词的一个片段包含一元和有限的二元谓词;和命题Lukasiewicz无限值概率逻辑
2019-05-14 cs.AI cs.LO
A modest proposal: explicit support for foundational pluralism
虽然数学家默认采用经典推理原则，但他们在工作时经常切换上下文，将自己限制在各种形式的亚经典推理中。这种模式在逻辑学家和集合理论家中特别常见，但工作数学家也经常这样做，例如，“下面的证明是建设性的”或“下面的证明不使用选择”。然而，目前的证明助手提供的正式捕获这些叙述性笔记，观察，尤其是真实的戈登的HOL，一个经典的高阶逻辑的基础上的系统的支持。因此，具有讽刺意味的是，HOL和它的许多实现似乎比主流数学家更致力于经典推理，限制了人们可以轻松形式化的数学内容。为了促进这些上下文切换，我们建议数学家在暂时进行次经典工作时在心理上使用一个简单的污染系统--这是一个目前在证明助手中没有探索的想法。我们引入了一系列适度的，但影响深远的变化HOL，扩展标准的两个地方的自然演绎关系，将一个污点标签，从一个特定的晶格，并描述或限制的“量”的经典推理中使用的证明。Taint既可以被看作是HOL证明上的一个简单的类型系统，也可以被看作是证明树上的一种静态分析形式，它将我们的逻辑划分为不同表达能力的各种片段，并排放置。结果可以从一个“不太经典”的片段传递到一个“更经典”的逻辑片段而不进行修改，但反之亦然，结果在世界之间的流动由一个类似于子类型或包容规则的推理规则控制。
2023-02-20 cs.LO cs.PL
Reasoning about Explanations for Negative Query Answers in DL-Lite
Free University of Bozen-Bolzano（博尔扎诺-博岑自由大学）；Vienna University of Technology（维也纳工业大学）；University of Oxford（牛津大学）
为了满足可用性需求，大多数基于逻辑的应用程序提供推理服务的解释设施。这也适用于描述逻辑，其中研究集中在TBox推理和最近的查询回答的解释上。除了解释查询答案中元组的存在之外，解释为什么给定的元组丢失也很重要。我们解决后一个问题，例如，通过采用溯因推理，在DL-Lite本体上进行合取查询回答;也就是说，我们寻找ABox的补充，强制给定的元组出现在结果中。作为推理任务，我们考虑存在和承认的解释，相关性和必要性的一个给定的声明的解释。我们刻画了这些问题的计算复杂性的任意，子集最小，基数最小的解释。
2014-02-04 cs.AI cs.LO
Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)
University of Luxembourg（卢森堡大学）
本文基于LogiKEy逻辑多元知识表示与推理方法论，主张在统一元逻辑框架内支持对象逻辑层面的逻辑多元主义，并警告逻辑帝国主义对跨学科复用的阻碍。
2026-05-26 cs.AI cs.LO math.LO
View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version)
持久内存的兴起正在颠覆计算的核心。我们的工作旨在帮助程序员导航这个勇敢的新世界，通过提供一个程序逻辑推理x86代码，使用低级操作，如内存访问和围栏，以及持久化原语，如刷新。我们的逻辑，Pierogi，受益于一个简单的底层操作语义的基础上的意见，能够处理优化的刷新操作，并在伊莎贝尔/HOL证明助手机械化。我们详细介绍了Pierogi的证明规则，并证明了它们的声音。我们还展示了如何Pierogi可以用来推理一系列具有挑战性的单线程和多线程持久程序。
2022-01-15 cs.LO cs.PL
Learning-Assisted Automated Reasoning with Flyspeck
University of Innsbruck（因斯布鲁克大学）；Radboud University（拉德堡德大学）
Flyspeck项目编码的大量数学知识与外部自动定理证明器（ATP）和在证明上训练的机器学习前提选择方法相结合，产生了能够自动回答各种数学查询的AI系统。该架构的性能评估在一个自举方案模拟Flyspeck的发展，从公理到最后定理，每次只使用以前的定理和证明。结果表明，39%的14185定理可以证明在一个按钮模式（没有任何高层次的建议和用户交互）在30秒的实时的在一个14 CPU的工作站。必要的工作包括：（i）实现HOL Light逻辑到ATP形式主义的合理翻译：无类型的一阶、多态类型的一阶和有类型的高阶，（ii）从HOL Light和ATP证明导出依赖信息用于机器学习器，以及（iii）选择合适的表示和方法用于从以前的证明学习，以及它们作为顾问与HOL Light集成。这项工作的描述和讨论在这里，并提供了一个初步的分析机构的证明，发现完全自动。
2014-10-26 cs.AI cs.DL cs.LG
Transfinite Modal Logic: a Semi-quantitative Explanation for Bayesian Reasoning
Japan Advanced Institute of Science and Technology（日本北陆先端科学技术大学院大学）
贝叶斯推理在人类理性和机器学习中起着重要的作用。本文介绍了超限模态逻辑，它将模态逻辑与序数运算相结合，半定量地形式化贝叶斯推理。在技术上，我们首先研究了序数算术的一些非平凡性质，然后使我们能够自然和优雅地扩展正常模态逻辑的语义到新的超限模态逻辑上，同时仍然保持Kripke模型的普通定义完全不变。尽管所有的超限数学定义，我们认为，在实践中，这种逻辑实际上可以适应一个完全有限的解释。我们认为，超限模态逻辑以一种相当简单明了的形式抓住了贝叶斯推理的本质，特别是它为福尔摩斯的名言“当你排除了不可能，剩下的无论多么不可能，都一定是真理”提供了一个完美的解释。“我们还证明了我们的逻辑的有限模型性质定理的对应。
2022-04-02 cs.AI cs.LO math.LO
Logical Modalities within the European AI Act: An Analysis
University of Bamberg（巴姆堡大学）；Freie Universität Berlin（柏林自由大学）
本文分析《欧洲人工智能法案》中的逻辑模态，借助LogiKEy、HOL与Isabelle/HOL构建逻辑嵌入并编码示例条款，以评估其自动推理适用性及挑战。
2025-05-12 cs.AI cs.CY cs.LO
