Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs
Aarhus University（奥胡斯大学）；New York University（纽约大学）
研究对抗性概率程序，提出埃尔顿这一高阶分离逻辑，利用语言层面延迟采样和逻辑层面瓮资源等工具，结合其他特性，能证明安全示例错误界限，且证明已机械化验证。
2026-07-16 cs.LO cs.PL
Mechanised Hypersafety Proofs about Structured Data: Extended Version
本文提出 Hoare 风格关系分离逻辑 LGTM，将结构化数据操作规范为参数化超安全性，并在 Coq 中机械化其理论与策略，验证了13个压缩数组和稀疏张量案例。
2024-04-09 cs.LO cs.PL
A two-level logic approach to reasoning about computations
关系描述已被用于形式化不同的计算概念，包括，例如，操作语义，类型，和接受非确定性机器。因此，我们提出了一个（限制）的逻辑理论的关系作为一种语言来指定这样的概念。我们的规范逻辑的进一步特点是能够显式地处理对象语言中的绑定。一旦这样的逻辑被固定，下一个自然的问题是我们如何证明关于用它写的规范的定理。我们建议使用第二种逻辑，称为推理逻辑，用于此目的。一个令人满意的推理逻辑应该能够完全编码规范逻辑。与规范逻辑相关的是各种绑定概念：公式中的量词，序列中的特征变量，以及术语中的抽象。为了提供这些方面的自然处理，推理逻辑必须编码绑定结构以及它们的范围，自由和绑定变量以及捕获避免替换的相关概念。此外，为了支持有关可证明性的论点，推理逻辑应该拥有通过归纳和协同归纳构建证明的强大机制。我们提供这些功能，在这里使用一个逻辑称为G表示的关系，通过原子判断的定义，包含推理规则的归纳和共归纳，并包括一个特殊的通用量词的条件。我们展示了如何证明在规范逻辑可以透明地编码在G。我们还描述了一个交互式定理证明称为阿贝拉，实现G和这种两级逻辑方法，我们提出了几个例子，证明阿贝拉在推理计算的功效。
2010-09-01 cs.LO cs.PL
Reasoning About Higher-Order Relational Specifications
遗传Harrop公式（HH）的逻辑已被证明可用于指定广泛的形式系统。这种逻辑包括一种形式的假设判断，导致动态变化的假设集，这是关键的编码边条件和上下文，经常出现在结构操作语义（SOS）风格的介绍。规格说明在推理它们所描述的系统时通常是有用的。Abella定理证明器通过在丰富的推理逻辑中显式地嵌入规范逻辑来支持这种推理;然后通过这种嵌入来推理规范。然而，实现感应原理在面对动态变化的假设集是不平凡的，原来的Abella系统只使用了一个子集的HH规范逻辑的原因。我们在这里开发了一种方法，支持所有HH归纳推理。我们的方法利用HH的聚焦属性来隔离假设的使用和在推理逻辑中对任何这样的假设的结构进行特征化的能力。我们证明了这些想法的有效性，通过几个规范和元理论推理的例子，已实施的扩展版本的Abella。
2013-08-05 cs.LO
Biform Theories: Project Description
双形式理论是公理理论和算法理论的结合，支持推理和计算的集成。对于指定和推理操作数学表达式的算法，这些是理想的。然而，形式化的biform理论是具有挑战性的，因为它需要的手段来表达语句的相互作用，这些算法做什么，他们的行动意味着什么数学。本文描述了一个项目，以开发一种方法来表达，操纵，管理和生成数学知识作为一个网络的双形理论。它是MathScheme的一个子项目，MathScheme是麦克马斯特大学的一个长期项目，旨在创建一个集成形式演绎和符号计算的框架。
2018-06-12 cs.LO
Possible values: exploring a concept for concurrency
并发中的一个重要问题是干扰。这个问题表现在共享变量和基于通信的并发-本文重点放在前一种情况下，干扰是由环境的进程改变共享变量的值。可靠/保证的方法已被证明是有用的，在指定和推理组合的并发程序。本文探讨了使用“可能值”符号推理变量的值可以改变多次干扰。这个概念除了在提供清晰的规范方面的价值外，它还提供了一种原则性的方法，避免了对一些辅助（或幽灵）变量的需要，这些变量的不明智使用会破坏组合性。
2016-01-09 cs.LO
Lifted Relational Algebra with Recursion and Connections to Modal Logic
我们提出了一种新的形式主义，用于指定和推理的问题，涉及异构的“信息块”-大型数据集，任何类型的决策程序和复杂性和它们之间的连接。我们的建议的本质是解除Codd的关系代数从关系表上的操作到结构类上的操作（递归），并添加一个方向的信息传播。我们观察到存在的信息传播在几个形式主义有效的推理，并用它来表达一元否定和操作中使用的图形数据库。我们仔细分析了几个推理任务，并建立了一个精确的广义查询评估和时态逻辑模型检验之间的联系。我们的发展使我们能够揭示经典和模态逻辑之间的一般对应关系，并可能揭示一个新的光模态逻辑和相关形式的良好的计算性能。
2016-12-29 cs.AI cs.DB cs.LO
Reasoning about Temporary Coalitions and LTL-definable Ordered Objectives in Infinite Concurrent Multiplayer Games
我们建议加强使用命题表示的决定和战略，如CTL* 建立时间的语言，如果解释并发游戏模型。该增强功能允许指定不同的联盟结构。在量化的CTL* 这种技术也可以量化联盟结构，我们用它来量化一个扩展形式的战略配置文件，捕捉临时联盟。我们还扩展CTL* 的一个时间形式的二元偏好算子，可以追溯到冯赖特的工作。由此产生的量化CTL* 的扩展可以用来阐明并发多人游戏中行为的合理性条件，例如出现在解决方案概念中的行为，玩家有多个个人目标和偏好，并考虑到形成临时联盟的可能性。我们提出了完整的公理化扩展CTL* 的时间偏好算子。逻辑的可判定性不受这种扩展的影响。
2020-11-07 cs.LO cs.MA
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
Karlsruhe Institute of Technology (KIT)（卡尔斯鲁厄理工学院）
针对多语言系统性质验证难题，本文提出异构动态逻辑(HDL)框架，通过提升与组合操作模块化整合不同程序逻辑，形式化证明推理规则可靠性与相对完备性，并借由汽车控制器案例展示跨语言推理的实用价值。
2026-04-14 cs.LO cs.PL
Concurrent Data Structures Linked in Time
关于并发数据结构的正确性的论证通常通过使用线性化的概念并指定数据结构的过程的线性化点来执行。这种参数通常是麻烦的，因为线性化点的时间位置可以是动态的（取决于干扰、运行时值和来自过去甚至未来的事件）、非本地的（出现在所考虑的过程之外的过程中），并且其在执行跟踪中的位置只能在所考虑的过程已经终止之后确定。在本文中，我们提出了一种新的方法，基于分离式逻辑，推理并发对象的线性化点。我们接受线性化点的动态特性，并将其编码为数据结构的辅助状态的一部分，以便当发生某些适当的运行时事件时，可以根据需要通过辅助代码在适当的位置动态修改它。我们把这个想法命名为时间链接，因为它把时间推理简化为空间推理。例如，修改线性化点的时间位置可以类似于分离逻辑中的指针更新来建模。此外，辅助状态提供了一种方便的方式来简明地表达对此类并发对象的客户端进行推理所必需的属性。我们通过验证（在Coq中机械地）Jayanti以及一些客户端的复杂的最佳快照算法来说明该方法。
2017-01-18 cs.DC cs.LO cs.PL
Mechanizing Matching Logic In Coq
匹配逻辑是使用模式和模式匹配来指定和推理数学结构的形式体系。它越来越流行，已被用来定义许多逻辑系统，如具有递归定义的分离逻辑和线性时态逻辑。此外，它还作为K语义框架的逻辑基础，该框架用于为许多现实世界的语言构建实用的验证器。尽管匹配逻辑是一个容纳大量理论的基本形式系统，但它缺乏通用的、机器检查的形式化。因此，我们使用Coq证明助手来形式化匹配逻辑。具体来说，我们创建了一个新的表示匹配逻辑，使用本地无名编码，我们正式的语法，语义和证明系统，这种表示在Coq证明助手。最重要的是，我们证明了形式化证明系统的可靠性，并提供了一种在Coq中进行交互式匹配逻辑推理的方法。我们相信这项工作提供了一个以前未探索的途径推理匹配逻辑，其模型和证明系统。
2022-09-21 cs.LO
Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs
需要一个带有量子变量的一阶逻辑作为断言语言，用于指定和推理量子程序的各种属性（例如正确性）。令人惊讶的是，这样的逻辑在文献中缺失，现有的一阶Birkhoff-von Neumann量子逻辑只处理经典变量和它们的量化。在本文中，我们填补了这一空白，通过引入一阶扩展的Birkhoff-von Neumann量子逻辑与泛量词和存在量词的量子变量。给出的例子表明，我们的逻辑特别适合于指定量子计算和量子信息中研究的一些重要性质。我们进一步将此逻辑作为断言逻辑纳入量子霍尔逻辑中，使其能起到类似于经典霍尔逻辑中的一阶逻辑和分离逻辑中的BI-逻辑的作用。特别是，我们展示了它如何可以用来定义和推导量子概括的一些适应规则，已被应用于显着简化验证的经典程序。预计本文中定义的断言逻辑-一阶量子逻辑与量子变量-可以与各种量子程序逻辑相结合，作为一个坚实的逻辑基础上，验证工具可以建立使用证明助手，如Coq和Isabelle/HOL。
2022-05-04 cs.LO cs.PL quant-ph
Presentable signatures and initial semantics
本文提出可呈现签名框架，用于指定数据类型和编程语言语法，通过初始语义生成语法，涵盖变量绑定并支持组合构造，且经计算机验证。
2021-05-25 cs.LO cs.PL
Matching Logic
本文提出了匹配逻辑，一个一阶逻辑（FOL）的变种，通过模式和模式匹配来指定和推理结构。它的句子，模式，是由变量，符号，连接词和量词构成的，但功能和谓词符号之间没有区别。在模型中，模式计算到幂集域（与之匹配的一组值），而FOL中的函数和谓词映射到常规域。匹配逻辑统一地概括了几个对程序分析很重要的逻辑框架，例如：命题逻辑、代数规范、具有等式的FOL、模态逻辑和分离逻辑。模式可以在任何程序配置中的任何级别指定分离要求，而不仅仅是在堆或存储中，而不需要任何特殊的逻辑结构：模式匹配的本质是，如果两个结构作为模式的一部分进行匹配，那么它们只能在空间上分离。与FOL一样，匹配逻辑也可以被转化为具有相等性的纯谓词逻辑，同时承认它自己的健全和完整的证明系统。匹配逻辑的一个实际方面是，具有等式的FOL推理仍然是合理的，因此现成的证明器和SMT求解器可以用于匹配逻辑推理。匹配逻辑特别适合于对具有操作语义的程序设计语言中的程序进行推理，但不限于此。
2017-12-17 cs.LO
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
并发Kleene代数是一个优雅的工具，用于并发程序的等式推理。CKA缺少的并发程序的一个重要特性是限制合法交织的能力。为了弥补这一点，我们扩展了标准模型的CKA，即pomsets，一个新的功能，所谓的盒子，它可以指定该系统的一部分是保护免受外界干扰。我们研究了这个新模型的代数性质。CKA的另一个缺点是用于表达程序属性的语言与用于表达程序本身的语言相同。对于实际目的来说，这通常限制太多。我们提供了一个逻辑，“pomset逻辑”，这是一个断言语言，用于指定这些属性，并解释pomset与框。与其他方法相比，这种逻辑不是基于状态的，而是表征程序的运行时行为。我们开发的基本元理论的pomset逻辑和CKA之间的关系，包括框架规则，以支持本地推理，并说明这种关系与简单的例子。
2020-05-06 cs.LO
Quantum Hoare Type Theory
随着量子计算机成为现实，现在是时候提出有效的技术来帮助程序员编写正确的量子程序了。受经典计算中Hoare类型论的启发，我们提出了量子Hoare类型论（QHTT），它可以在计算类型内提供关于量子态修改的精确规范。霍尔类型中的这些规范以霍尔逻辑风格的前置条件和后置条件的形式给出，遵循命题作为类型原则。类型检查过程验证实现是否符合所提供的规范。QHTT有可能成为一个统一的系统，用于编程，指定和推理量子程序。
2021-11-15 cs.ET cs.LO cs.PL
Combining Deduction Modulo and Logics of Fixed-Point Definitions
归纳和共归纳规范在计算系统的形式化中有着广泛的应用。这样的规范在支持定点定义的逻辑中有一个自然的再现。另一个有用的形式化手段是递归规范。这些规范不直接由定点推理技术补充，相应地，不必满足强单调性限制。我们将展示如何将重写功能到逻辑的定点定义对另外支持递归规范。特别是，我们描述了一个自然的演绎演算，增加了一种形式的“封闭世界”的平等-一个关键的成分，以支持定点定义-演绎模，一个框架，用于扩展一个逻辑与重写层操作公式。我们表明，我们的演算具有很强的规范化时，重写系统满足一般属性，我们证明了它的有用性，在指定和推理基于语法的描述。将封闭世界等式整合到演绎模中，使我们重新配置了这种形式的等式的消除原理，第一次解决了关于归约下有限证明的稳定性问题。
2012-04-27 cs.LO
Embedding Differential Dynamic Logic in PVS
本文提出将微分动态逻辑（dL）嵌入原型验证系统（PVS）中，形式化了混合程序语义与证明演算，构建了Plaidypvs以支持在PVS内部验证混合程序并推理整类程序。
2024-04-23 cs.LO
On the construction of multi-valued concurrent dynamic logic
动态逻辑是对命令式程序进行推理的强大框架。引入了一个带有并发操作符的扩展[18]来形式化并行运行的程序。在另一个方向上，其他作者提出了一个系统的方法来生成多值命题动态逻辑来推理加权程序[14]。本文介绍了这两个框架相结合，在并发计算中引入不确定性的第一步。在开发的框架中，权重被分配给并行执行的每个分支，导致模糊编程范式固有的（可能的）非对称并行性[21，2]。通过采用这样的方法，得到了一族逻辑，称为多值并发命题动态逻辑（CGDL（A）），参数上的动作格A指定的“权重”的概念分配给程序执行。此外，还讨论了CPDL中某些公理在新的生成逻辑族中的有效性。
2019-11-01 cs.LO
BayesL: a Logical Framework for the Verification of Bayesian Networks
University of Twente（特文特大学）；University of Urbino（乌尔比诺大学）；Radboud University（拉德堡德大学）
本文提出BayesL逻辑框架，用于形式化表达、查询和验证贝叶斯网络的行为，通过支持概率推断和模型检查查询，提升贝叶斯网络的透明度和可靠性。
2026-04-28 cs.AI cs.LO
Eventual Discounting Temporal Logic Counterfactual Experience Replay
Caltech（加州理工学院）；Penn State（宾夕法尼亚州立大学）；Latitude AI（Latitude人工智能公司）
线性时序逻辑（LTL）提供了一种简化的方式来指定策略优化的任务，否则可能难以用标量奖励函数来描述。然而，标准RL框架可能过于短视，无法找到最大限度的LTL满足政策。本文有两个贡献。首先，我们开发了一个新的价值函数为基础的代理，使用一种技术，我们称之为最终折扣，根据该技术可以找到满足LTL规范的政策，以最高的可实现概率。其次，我们开发了一种新的经验重放方法，通过反事实推理的不同方式来满足LTL规范，从政策上的推出生成政策外的数据。我们的实验，在离散和连续的状态-动作空间进行，证实了我们的反事实经验重放方法的有效性。
2023-03-03 cs.AI cs.LG cs.LO
Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
本文提出参数化动态逻辑DLp，通过引入程序配置标签支持符号执行与语法结构推理，构建循环预证明系统保证无限证明树可靠性，为通用程序规约与验证提供灵活框架。
2025-01-29 cs.LO cs.SE
Dynamic Term-Modal Logics for First-Order Epistemic Planning
DTU Compute, Technical University of Denmark（丹麦技术大学DTU计算学院）；London School of Economics（伦敦政治经济学院）；Center for Information and Bubble Studies, University of Copenhagen（哥本哈根大学信息与泡沫研究中心）
许多经典的规划框架都是建立在一阶语言之上的。一阶表达能力对于通过模式表示动作的压缩性和指定量化条件（如$\neg\exists x\mathsf{blocks\_door}(x)$）是理想的。相反，最近的几个认知规划框架是建立在命题认知逻辑。认知语言对于描述涉及高阶推理或认知目标（如$K_{a}\neg\mathsf{problem}$）的规划问题很有用。本文提出了一个动态认知逻辑（DEL）的一阶版本。在这个框架中，例如，$\exists xK_{x}\exists y\mathsf{blocks\_door}(y)$是一个公式。形式主义相结合的DEL（高阶推理）与一阶逻辑（提升表示）的优势，多智能体认知规划模型。本文介绍了一种认知语言与可能世界的语义，其次是新的动态一阶动作模型和它们的执行，通过产品更新。利用一阶机制，认知行动模式的定义，以提供紧凑的，独立于问题的域描述，在PDDL的精神。关于元理论，本文定义了公理化的正常项模态逻辑，显示了一个典型的模型定理的结果，它允许建立完整性通过框架特征公式，有限代理的情况下，显示可判定性，并显示了一般的完整性结果的动态扩展减少公理。
2020-06-02 cs.AI cs.LO cs.MA
