A proof theoretic basis for relational semantics
逻辑已被证明是必不可少的正式建模软件为基础的系统。这种形式化的描述，通常被称为规范，不仅作为需求文档和形式化，而且还为它们的分析和自动推理工具的开发提供了数学基础。逻辑学通常从其内在的两个方面来研究：句法和语义。后者的相关性在于这样一个事实，即对现实世界的现象进行逻辑描述，需要人们就人类如何解释和理解这些描述达成一致，以便系统可以根据其规范自信地构建。在更实际的方面，句法和语义之间的元逻辑关系决定了人们可以从某些分析技术的应用中得出的结论的重要方面，如模型检验。抽象模型理论（Abstract Model Theory）关于逻辑语言语义的数学观点）对于软件工程努力几乎没有实用价值。从我们的观点来看，值（可以分配给常量和变量的值）不应该仅仅是柏拉图式解释域中的点，而是可以通过规范签名上的术语命名的元素。简而言之，我们对那些需要任何语义信息而无法用可用语法表示的属性不感兴趣。在本文中，我们提出了一个框架，支持证明理论的形式化类的关系模型的行为逻辑语言，其域的话语保证只形成命名值。
2021-07-17 cs.LO
Presheaf Models of Relational Modalities in Dependent Type Theory
本报告是“桥/路径三次集的参数依赖类型论模型”（Nuyts，arXiv：1706.04383）的扩展。本文的目的是证明我们的依赖类型论模型的所有技术方面，参数量词（Nuyts，Vezzosi和Devriese，2017）和相关度（Nuyts和Devriese，2018）。
2018-05-17 cs.LO
Quantum Relational Hoare Logic
我们提出了一个逻辑的推理对互动的量子程序-量子关系霍尔逻辑（qRHL）。这种逻辑遵循概率关系霍尔逻辑（Barthe et al. 2009）的精神，并允许我们在给定输入关系的情况下，用公式表示两个量子程序的输出如何相关。概率RHL被广泛用于经典密码协议的计算机验证安全性证明。由于pRHL不适合分析量子密码，我们提出qRHL作为替代，适合后量子密码和量子协议的安全性分析。qRHL的设计对量子设置提出了一些独特的挑战，例如，量子寄存器上相等的定义。最后，我们实现了一个工具来验证qRHL中的证明，并在其中开发了几个示例安全证明。
2019-01-14 cs.LO quant-ph
A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic
本文提出在概率关系霍尔逻辑中直接证明惰性采样程序不可区分性的新方法，无需急切采样转换及相关假设，并在EasyCrypt中实现验证。
2023-11-28 cs.CR cs.FL cs.LO
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
本文提出ReLoC Reloaded，一种基于Iris框架的机械化关系分离逻辑，用于证明高阶状态与细粒度并发程序的精化关系，并扩展了逻辑原子关系规范，支持预言变量以增强实用性。
2021-07-20 cs.LO cs.PL
Relational Connectors and Heterogeneous Bisimulations
本文在泛代数框架下引入集合函子间的关系连接子，建立不同类型系统间的异构互模拟理论，并证明Hennessy-Milner型定理，应用于带标签迁移系统、概率系统及输入/输出一致性等场景。
2025-02-06 cs.LO
Polymorphic type inference for the relational algebra
给出了关系代数的多态性解释。我们介绍了一种专门为关系代数表达式调整的“类型公式”的形式主义，并提出了一种算法，用于计算给定表达式的“主要”类型。表达式的主类型是一个公式，它以清晰简洁的方式指定所有类型（属性集）到关系名称的赋值，在此条件下，给定的关系代数表达式是良好类型的，以及表达式在每个赋值下的输出类型。讨论的主题包括复杂性和多态表达能力。
2001-06-14 cs.DB cs.LO
Synthesizing Nested Relational Queries from Implicit Specifications
派生数据集可以隐式或显式定义。（数据集$\vec{I}$方面的数据集$O$的）隐式定义是涉及源数据$\vec{I}$和接口数据$O$的逻辑规范。如果规范的任何两个模型在$\vec{I}$上达成一致，则它是$O$在$\vec{I}$方面的有效定义。相反，显式定义是从$\vec{I}$生成$O$的查询。贝丝定理的变体指出，可以将隐式定义转换为显式定义。此外，这种转换可以有效地完成，在一个合适的证明系统中证明隐含的可定义性。我们证明了嵌套关系的类似的有效的隐式到显式的结果：隐式定义，在嵌套关系的自然逻辑，可以有效地转换为显式定义的嵌套关系演算NRC。因此，我们可以有效地提取重写的NRC查询的NRC意见方面，证明了该查询是由意见。
2022-09-17 cs.DB cs.LO
Graphs of relational structures: restricted types
约束满足问题（CSP）的代数方法使用关系结构的高阶对称性-多态性-来研究CSP的复杂性。在本文中，我们进一步发展的方法之一，代数方法可以实现，并将其应用到一些类型的CSP。这种方法在我们的LICS 2004论文中介绍，涉及有限代数和关系结构的局部结构的研究。它将一个代数A或一个关系结构S与一个图联系起来，图的顶点是A（或S）的元素，边表示A的子集，使得A的某些项运算的限制在子集上是“好的”，即充当三种类型之一的运算：半格、多数或仿射。在本文中，我们使用这一理论，并考虑代数的边缘从一个限制的类型集。我们证明了标准代数结构下的类型限制。然后，我们表明，如果在一个关系结构中的类型边是受限制的，那么相应的CSP可以解决在多项式时间通过特定的算法。特别是，我们给出了一个新的，有点更直观的证明有界宽度定理：CSP代数A有界宽度当且仅当A不包含仿射边。实际上，这个结果表明有界宽度意味着宽度（2，3）。最后，证明了无半格边代数的幂子代数很少，即这类代数上的CSP也是多项式时间的。本文所得到的方法和结果是作者2017年证明二分法猜想的重要组成部分。二分法猜想也被朱克独立证明。
2020-07-20 cs.LO
Full Definability in a Profunctorial Model
Chiba University（千叶大学）；Tohoku University（东北大学）；University of Edinburgh（爱丁堡大学）；Kyoto University（京都大学）
本文研究了基于群oid上仿射范畴的模型中的全可定义性，证明了稳定且全的仿射在多价线性逻辑中可通过证明网络定义。
2026-04-29 cs.LO
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
MapReduce框架被广泛用于实现分布式算法。然而，将命令式算法转换为这些框架需要对算法进行重大的结构更改。由于大规模运行错误算法的成本可能是严重的，因此非常希望验证翻译的正确性，即，证明MapReduce版本与命令式版本等价。我们提出了一种新的方法来证明命令式和MapReduce算法之间的等价性的基础上划分的等价性证明到一个序列的等价性证明之间的中间程序具有较小的差异。我们的方法是基于这样的见解，即需要两种子证明：（1）改变控制流结构的统一变换，这些变换大多独立于它们所应用的特定上下文;以及（2）上下文相关的变换，这些变换不是统一的，但保留了整体结构，并且可以使用耦合不变量证明是正确的。我们证明了我们的方法的可行性，通过评估它的两个原型算法通常用作MapReduce框架中的例子：k-means和PageRank。为了进行证明，我们使用交互式定理证明器Coq与部分证明自动化。结果表明，我们的方法及其基于Coq的原型实现，使非平凡算法的等价性证明，并可以在很大程度上自动化。
2018-01-26 cs.LO cs.PL cs.SE
Proving uniformity and independence by self-composition and coupling
耦合证明是一种经典的证明技术，用于建立两个概率过程的概率性质，如随机优势和马尔可夫链的快速混合。最近，耦合已被调查作为一个有用的抽象形式化推理的概率程序的关系属性，特别是建模约简为基础的密码学证明和验证差分隐私。在本文中，我们证明了概率耦合可以用于验证非关系的概率属性。具体来说，我们表明，程序逻辑pRHL-其证明是正式版本的耦合证明-可用于形式化的一致性和概率独立性。我们使用EasyCrypt证明助手正式验证我们的主要示例。
2017-04-01 cs.LO cs.PL
Paraconsistent logic and query answering in inconsistent databases
本文提出用亚相容逻辑LPQ$^{\supset,\mathsf{F}}$处理不一致数据库中的查询，无需数据库修复即可定义一致答案，并给出序列演算证明系统以支持证明搜索算法。
2023-03-11 cs.DB cs.LO
Appendix for: Cut-free Calculi and Relational Semantics for Temporal STIT logics
Technische Universität Wien（维也纳技术大学）
本文是Berkel和Lyon于2019年发表的论文“时态STIT逻辑的免切演算和关系语义”的附录。给出了基本STIT逻辑Ldm（相对于非自反的时态Kripke STIT框架）的完备性证明，并推导了逻辑Xstit的主体独立性公理.
2019-02-18 cs.AI cs.LO
Parametric Cubical Type Theory
我们展示了一个计算类型论，它结合了高维结构的carnivical立方类型论的内部参数化原语的参数类型论，绘制出两者之间的相似性和区别。结合理论既支持一价性，也支持它的关系等价物，我们称之为相对论。我们展示了使用的理论，通过分析多态类型，包括更高的归纳类型之间的功能，我们通过例子展示了如何相对性可以用来表征归纳类型的关系解释。
2019-07-08 cs.LO
Relational Cost Analysis for Functional-Imperative Programs
关系成本分析旨在正式建立两个项目评估成本差异的界限。作为一个特殊的情况下，也可以使用关系成本分析，以建立在两个不同的输入相同的程序的评估成本的差异的界限。执行关系成本分析的一种方法是使用关系类型和效果系统，该系统支持对两个程序的两次执行之间的关系进行推理。基于这一基本思想，我们提出了一个类型和效果的系统，称为ARel，推理数组操作，高阶函数命令式程序的相对成本。我们的方法的关键成分是一个新的轻量级类型细化规则，我们使用它来跟踪两个数组之间的关系（差异）。这种纪律结合霍尔风格的三元组内置的类型，使我们能够表达和建立精确的相对成本的几个有趣的程序，迫切需要更新他们的数据。
2019-09-24 cs.LO cs.PL
Reasoning about proof and knowledge
在以前的工作[Lewitzka，日志。J. IGPL 2017]，我们提出了一个经典模态系统的层次结构，以及代数语义，用于推理直觉真理，信念和知识。偏离哥德尔在S4中对IPC的解释，我们的模态系统以[Lewitzka，J. Log. Comp.2015]。模态算子可以被看作是直觉真理的谓词，即证明。认识论原则部分采用直觉主义认识论逻辑IEL [Artemov and Protopescu，Rev. Symb. Log. 2016年]。在本文中，我们表明，我们的层次结构的S5风格的系统对应于一个扩展的Brouwer-Heyting-Kolmogorov解释，是完整的w.r.t.一种基于直觉一般框架的关系语义。在这个意义上，我们的S5风格逻辑是充分和完整的系统，用于结合信念或知识进行证明的推理。建议的关系语义是一个统一的框架，也IEL可以建模。IEL形式化的基于验证的直觉知识是我们的S5风格系统所描述的知识的一个特例。
2018-12-28 cs.LO
Thirty-seven years of relational Hoare logic: remarks on its principles and history
关系霍尔逻辑扩展了模块化演绎验证的适用性，以涵盖重要的2-运行属性，包括依赖性要求，如机密性和程序关系，如程序版本之间的等效性或相似性。相当数量的最近的作品介绍了不同的关系霍尔逻辑尚未收敛到一套核心的证明规则。本文回顾了鲜为人知的早期工作。这揭示了一些原则，澄清和组织的规则，以及建议一个新的规则和完整性的新概念。
2022-07-16 cs.LO cs.PL
Modal reduction principles across relational semantics
本文建立了系统的联系，一阶对应的Sahlqvist模态约简原则在各种关系的语义设置，其中包括脆和多值Kripke框架，脆和多值极性为基础的框架（又名丰富的形式背景）。建立在统一对应理论，我们的目标是引入一个理论环境，使之有可能：（a）比较和相互关联的各种框架对应（b）识别不同类型关系结构的框架对应语言中的一阶句子何时编码相同的“模态内容”;（c）在不同的语义语境中有意义地传递和表示众所周知的关系属性，如反身性、传递性、对称性、连续性、汇合性、密度。这些结果可以被理解为研究计划的第一步，该计划旨在使对应论不仅（方法上）统一，而且（有效地）参数化。
2023-02-13 cs.LO
A General (Uniform) Relational Semantics for Sentential Logics
University of Thessaly（色萨利大学）
本文提出了一种通用的关系语义学框架，通过公理化和结构的调整，为经典和非经典逻辑提供统一语义，并利用广义Sahlqvist-van Benthem算法进行对应结果计算。
2025-11-23 cs.LO math.LO
An Elementary Proof of the FMP for Kleene Algebra
Open Universiteit（开放大学）；Institute for Logic, Language and Computation (ILLC) at the University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）；LIACS Leiden University（莱顿大学计算科学实验室）
本文通过变换自动机的方法，给出了Kleene代数有限模型性质的初等证明，并推导出Kozen和Pratt定理。
2026-01-14 cs.FL cs.LO
Relational semantics of linear logic and higher-order model-checking
在这篇文章中，我们在高阶模型检验和线性逻辑之间建立了一种新的、有点出乎意料的联系。我们的出发点是观察到，一旦嵌入到线性逻辑的关系语义中，任何高阶递归方案（HORS）的Church编码都会与相同签名的交替树自动机（ATA）的对偶Church编码结合在一起。此外，HORS和ATA的关系解释之间的相互作用确定了一组接受状态的树自动机对无限树所产生的递归方案。我们将展示如何将这一结果扩展到交替奇偶自动机（APT）通过引入线性逻辑的指数模态的参数化版本，捕获高阶模型检验中颜色（或优先级）的形式属性。我们特别展示了如何重新理解以这种方式的类型理论的方法来高阶模型检验开发的小林和Ong。我们简要地解释在最后的文件如何驱动他的分析结果在一个新的和纯粹的语义证明的可判定性的公式的一元二阶逻辑的高阶递归计划。
2015-05-01 cs.LO cs.PL math.LO
Event Driven Computations for Relational Query Language
本文论述了一种扩展的计算模型，它使用参数化的数据对象的实体的家庭，并反映了这个问题的初步轮廓。在此基础上，本文选取了若干主题，进行了简要的分析和整理，以涵盖一个普遍性的问题.作者打算更多地讨论特定的主题，它们的相互联系和计算意义作为一个小组提案，所以这篇论文还没有被评估为封闭的期刊论文。为了节省篇幅，所有的技术和实现功能都留给以后的文件。数据对象是一个原理图实体，由部分函数建模。类型的概念由依赖于事件和类型的变量域扩展。可变域是从潜在的和示意性的个体构建的，并根据事件的序列生成有效的类型家族。每一个有效的类型都由相对于事件或脚本而言是真实的个体组成。如果类型依赖于脚本，则附加数据对象的相应视图，否则生成快照。由此确定的类型给出了类型化变量的上限，使得局部范围是事件驱动的，从而产生实际个体的家族。使用可拓关系和意向关系来扩展查询语言的表达能力。
2001-06-12 cs.DB cs.LO cs.PL
Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs
我们提出了一种程序推理的方法，它在程序及其验证条件之间插入一个附加层，即以声明形式表示的程序的外延。首先将程序翻译成其表示，随后从该表示生成验证条件。然而，即使在任何验证尝试之前（并且独立于任何验证尝试），人们也可以调查指称本身以洞察程序的“语义本质”，特别是看看指称是否确实给出了相信程序具有预期行为的理由。因此，在实际执行形式化验证之前，可以检测并修复程序和元信息中的错误。更具体地说，程序语义的关系方法，我们建模的程序作为一个二元关系的程序状态的影响。一个正式的演算是从一个程序中推导出一个逻辑公式，描述这种关系，并进行检查和操作。我们已经实现了这一想法在RISC ProgramExplorer，一个新的程序推理环境的教育目的，其中包括以前开发的RISC ProofNavigator作为一个交互式的证明助理的全面形式。
2012-02-22 cs.LO cs.MS cs.PL
