The WhyRel Prototype for Relational Verification
程序之间的互操作关系在各种验证环境中作为一项任务出现，例如优化转换，将新版本的程序与旧版本（回归验证）和不干扰。然而，现有的工具，它提供了一个高水平的自动化的成本限制的程序考虑的关系验证的程序动态分配的可变状态的支持并不好。另一方面，自动激活工具需要更多的用户交互，但可以验证更广泛的程序类别。本文介绍了WhyRel，一个基于关系区域逻辑的指针程序关系属性自动验证工具。WhyRel通过验证案例研究进行评估，依赖于由Why3平台编排的SMT求解器。案例研究包括建立表示独立的ADT，显示不干扰，并从最近的文献挑战的问题。
2023-03-25 cs.LO cs.PL
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
本文提出高阶近似关系分离逻辑 Approxis，通过误差信用支持概率高阶有状态程序的近似与精确等价推理，并在 Coq/Iris 中机械化验证安全与采样示例。
2024-12-03 cs.LO cs.PL
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
本卷包含第三届程序等价和关系推理研讨会（PERR）和第六届验证与综合霍恩子句研讨会（HCVS）的联合后续会议记录，分别于4月6日和7日在捷克共和国布拉格举行，作为ETAPS的附属研讨会。
2019-07-08 cs.LO
Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
本研究提出概率程序逻辑Bluebell，通过“联合条件化”新模态统一一元与关系推理风格，实现条件独立性与关系提升的交互建模，为概率程序验证提供新工具。
2024-12-12 cs.LO cs.PL
Relational Test Tables: A Practical Specification Language for Evolution and Security
广泛的有趣的程序属性是内在相关的，即，它们关联两个或更多个程序轨迹。两个突出的关系性质是安全信息流和条件程序等价。通过显示不存在非法信息流，可以证明机密性和完整性。等效性证明允许使用现有（可信）软件版本作为新修订版的规范。目前，由于缺乏合适的关系规约语言，实践者很难获得关系属性的验证。在以前的工作中，我们介绍了广义测试表的概念：一个基于表的规约语言的功能（非关系）属性的反应系统。在本文中，我们提出了关系测试表-规范的扩展广义测试表的关系属性的规范，这是指两个或多个程序运行或跟踪。回归测试表支持异步程序通过口吃运行。我们展示了关系测试表的适用性，使用它们的规范和验证的两个例子，从域的自动化产品系统。
2019-10-20 cs.LO cs.SE
Learning Distributional Programs for Relational Autocompletion
KU Leuven（荷语鲁汶大学）；Czech Technical University in Prague（布拉格捷克理工大学）
关系自动补全是指在多关系数据中自动填充某些缺失值的问题。我们解决这个问题的概率逻辑编程框架内的分布子句（DC），它支持离散和连续的概率分布。在这个框架内，我们引入了DiceML {一种从关系数据（可能有丢失的数据）中学习DC程序的结构和参数的方法。为了实现这一点，DiceML将统计建模和分布子句与规则学习集成在一起。DiceML的显着特点是：1）处理关系数据中的自动完成，2）学习用统计模型扩展的分布子句，3）处理离散和连续分布，4）可以利用背景知识，5）使用基于期望最大化的算法来处理丢失的数据。实证结果表明，该方法的承诺，即使有缺失的数据。
2021-07-05 cs.AI cs.LG cs.LO
Relational Logic with Framing and Hypotheses: Technical Report
关系属性出现在许多设置：相关的两个版本的程序，使用不同的数据表示，不干扰属性的安全性，等关系验证的主要成分，有关对齐对中间步骤，已被用于在许多伪装，但现有的关系程序逻辑的范围很窄。本文介绍了一种基于新语法的逻辑，它将产品程序编织在一起，以表达关系公式被断言的控制流点的对齐。正确性判断的特点假设与关系规范，由一个规则的链接过程的实现。该逻辑支持关于包含相似和不相似的控制和数据结构的程序对的推理。推理动态分配的对象支持的框架规则的基础上的框架条件服从SMT证明。我们证明了合理性，并勾勒出逻辑如何用于数据抽象，循环优化和安全的信息流。
2016-11-28 cs.LO
An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation & More
最近，作者提出了下近似逻辑推理的程序。到目前为止，所有这些逻辑都局限于对单个程序行为的推理。然而，存在许多过度近似的关系逻辑，用于对程序对进行推理并将其行为关联起来。我们提出了第一个下近似关系逻辑，简单的命令式语言IMP。我们证明了我们的逻辑是健全的和完整的。此外，我们展示了如何在这个逻辑推理可以分解成非关系推理下近似霍尔逻辑，反映Beringer的结果过近似的关系逻辑。我们说明了我们的逻辑在一些小的例子中，我们证明了不安全的存在。
2020-03-11 cs.LO
Verifying Relational Properties using Trace Logic
我们提出了一个逻辑框架，在命令式程序中的关系属性的验证。我们的工作是出于安全应用程序的关系属性，往往需要推理公式与量词交替。我们的框架减少了验证的关系属性的命令式程序的有效性问题到跟踪逻辑，一阶谓词逻辑的表达实例。跟踪逻辑从它的语法中提取它的表达能力，这允许在计算跟踪上表达属性。它的公理化支持程序执行中中间步骤的细粒度推理，特别是循环迭代。我们提出了一个算法来编码的语义程序，以及它们的关系属性的跟踪逻辑，然后显示如何一阶定理证明可以用来推理所产生的跟踪逻辑公式。我们的工作是在快速工具中实现的，并与来自安全领域的例子进行评估。
2019-08-12 cs.LO
Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
Max-Planck Institute for Security and Privacy (MPI-SP)（马克斯·普朗克安全与隐私研究所）；IMDEA Software Institute（IMDEA软件研究所）；Key Laboratory of System Software (Chinese Academy of Sciences)（中国科学院系统软件重点实验室）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；Eidgenössische Technische Hochschule (ETH) Zürich（苏黎世联邦理工学院）；Ludwig-Maximilians-Universität München（慕尼黑大学）；Munich Center for Quantum Science and Technology (MCQST)（慕尼黑量子科学与工程中心）
提出用于无限维量子及经典-量子程序的完整关系逻辑，以自伴无界线性关系建模断言，支持定量与定性推理，并通过收敛定理和无限维对偶定理证明完备性。
2026-07-02 cs.LO cs.PL quant-ph
A quantitative probabilistic relational Hoare logic
本文提出定量关系概率程序逻辑 eRHL，利用扩展非负实数断言突破 PRHL 与 apRHL 的随机性对齐限制，并证明其在程序等价、统计距离和差分隐私上的可靠完备性。
2025-01-08 cs.LO
Alignment Completeness for Relational Hoare Logics
关系霍尔逻辑（RHL）提供了推理程序之间关系的规则。几个RHL包括一个我们称之为序贯积的规则，它从普通霍尔逻辑（HL）的判断中推断出关系正确性判断。其他规则体现了合理的推理模式，并已被发现在实践中很有用，但连续产品是相对完整的本身（与HL）。作为一种更令人满意的方法来评估RHL，对齐完整性的概念，引入的归纳断言方法和产品自动机。对齐完整性的结果，考虑到几个不同的规则集。该概念可以用于指导RHL和关系验证器的设计，以用于更丰富的程序设计语言和对齐模式。
2021-04-30 cs.LO cs.PL
Quantum Relational Hoare Logic with Expectations
我们提出了量子关系霍尔逻辑的一个变体（Unruh，POPL 2019），它允许我们在前置和后置条件中使用“期望”。也就是说，当推理成对的程序时，我们的逻辑允许我们定量地推理满足了多少特定的前置/后置条件，这些条件指的是程序输入/输出之间的关系。
2021-07-12 cs.LO quant-ph
A Relational Program Logic with Data Abstraction and Dynamic Framing
饰Tony Hoare霍尔在1972年发表的一篇论文中阐述了隐藏不变量和模拟的基本概念。隐藏：封装数据表示的不变量不需要在包含模块API的规范中提及。模拟：可以通过使用封装状态上定义的耦合关系证明旧实现和新实现之间的模拟来确定新数据表示和实现的正确性。这些结果在语义上被形式化，并且是针对一个简单的状态模型，尽管该论文声称这可以扩展到包含动态分配的对象。近年来，已经取得了进展，正式的索赔，模拟，虽然主要是在语义的发展。在这篇文章中，隐藏和模拟结合了Hoare 1969年论文中的思想：程序逻辑。对于一个基于对象的语言与动态分配，我们引入了一个关系霍尔逻辑与状态框架条件，形式化封装，隐藏的不变量，和耦合，涉及两个实现。关系和其他断言用一阶逻辑表示。规范可以表达广泛的关系属性，如条件等价和不干扰解密。证明规则通过方便的对齐来促进关系推理，并且相对于传统的操作语义被示出为合理的。导出的链接程序等价性证明规则直接体现了表示独立性。具有代表性的例子的适用性证明使用基于SMT的实现。
2022-07-19 cs.LO cs.PL
Beyond Graph Neural Networks with Lifted Relational Neural Networks
Czech Technical University in Prague（布拉格捷克理工大学）
我们展示了一个声明式可微编程框架的语言的提升关系神经网络，其中小的参数化逻辑程序被用来编码关系学习的情况下。当呈现诸如各种形式的图形的关系数据时，程序解释器动态地展开可微计算图形以通过标准手段用于程序参数优化。从使用的声明式数据库抽象，这导致到紧凑和优雅的学习程序，与现有的程序方法直接操作的计算图的水平。我们说明了这个想法如何用于现有各种先进神经架构的有效编码，特别关注图神经网络（GNN）。此外，我们还展示了当代GNN模型如何轻松扩展到更高的关系表达能力。在实验中，我们通过与专门的GNN深度学习框架进行比较来证明正确性和计算效率，同时对现有GNN模型的学习性能进行了一些说明。
2020-07-13 cs.AI cs.LG cs.LO
Thirty-seven years of relational Hoare logic: remarks on its principles and history
关系霍尔逻辑扩展了模块化演绎验证的适用性，以涵盖重要的2-运行属性，包括依赖性要求，如机密性和程序关系，如程序版本之间的等效性或相似性。相当数量的最近的作品介绍了不同的关系霍尔逻辑尚未收敛到一套核心的证明规则。本文回顾了鲜为人知的早期工作。这揭示了一些原则，澄清和组织的规则，以及建议一个新的规则和完整性的新概念。
2022-07-16 cs.LO cs.PL
Forall-Exists Relational Verification by Filtering to Forall-Forall
Amazon Web Services（亚马逊网络服务）；Dartmouth College（达特茅斯学院）；Stevens Institute of Technology（史蒂文斯理工学院）
本文提出一种通过过滤充分性变换将∀∃关系验证转化为∀∀验证的方法，开发配套程序逻辑与bicom乘积程序形式，证明可靠性并实现原型，可复用现有自动主动验证工具处理非确定性下的关键∀∃属性。
2026-10-21 cs.LO cs.PL
Proving Expected Sensitivity of Probabilistic Programs
程序灵敏度，也称为Lipschitz连续性，描述了程序输入的微小变化如何导致输出的有界变化。我们提出了一个平均概念的概率程序的程序灵敏度-预期灵敏度-平均距离函数的概率耦合的两个输出分布从两个类似的输入。通过改变距离，期望灵敏度恢复概率函数灵敏度的有用概念，包括机器学习算法的稳定性和马尔可夫链的收敛性。此外，预期灵敏度满足清洁的组成特性，并可进行形式化验证。我们开发了一个关系程序逻辑称为$\mathbb{E}$ pRHL证明预期的灵敏度属性。我们的逻辑有两个关键思想。首先，关系前置条件和后置条件使用距离表示，这是典型布尔值（关系）断言的实值概括。第二，判断解释的期望耦合，一种新的，定量概括的概率耦合，支持组合推理。我们证明了我们的逻辑的例子超出了以前的关系逻辑。我们的主要例子形式化一致稳定的随机梯度方法。此外，我们证明了快速混合的概率模型的人口动态。我们还扩展了我们的逻辑与期望耦合的传递性原则，以捕获Bubley和Dyer的路径耦合证明技术，并从统计物理学中形式化快速混合的Glauber动力学。
2017-11-08 cs.LO cs.PL
Complete Quantum Relational Hoare Logics from Optimal Transport Duality
本文提出一种量子程序定量关系霍尔逻辑，基于最优传输对偶性证明其可靠性与完备性，并支持投影断言嵌入。
2025-01-25 cs.LO quant-ph
Neuro-Relational Programs: Unifying Queries and Neural Computation over Structured Data
ILLC, University of Amsterdam（伊拉斯谟罗素学院，阿姆斯特丹大学）；Leipzig University（莱比锡大学）；ScaDS.AI Center（ScaDS.AI研究中心）；Technion（技术学院）；RelationalAI（关系AI）
提出神经关系程序（NRP），一种扩展Datalog规则的声明式查询语言，通过嵌入操作融合关系推理与可学习神经组件，实现关系数据上的通用神经计算。
2026-10-16 cs.CC cs.DB cs.LG
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
本文提出Clutch，一种支持异步概率耦合的高阶概率关系分离逻辑，用于推理高阶程序的上下文精化与等价性，并在Coq中形式化验证。
2023-11-14 cs.LO cs.PL
Relational Verification via Invariant-Guided Synchronization
关系属性描述了一个或多个程序的多次执行之间的关系，例如功能等价。用于自动验证这些属性的常规方法通常依赖于基于语法的启发式策略，用于在输入程序中找到同步点。然后，这些同步点用适当的关系不变量进行注释，以完成证明。然而，当选择次优同步点时，所需的不变量可能是复杂的，甚至在目标理论中是无法表达的。在这项工作中，我们提出了一种新的方法来验证关系属性。该方法搜索同步点，同时合成关系不变量。具体来说，该方法使用合成的不变量作为指导，找到适当的同步点，导致一个完整的证明。我们实现了我们的方法作为一个名为PEQUOD的工具，它的目标是Java虚拟机（JVM）字节码。我们评估PEQUOD使用它来解决来自研究文献的验证挑战，并通过验证学生提交的解决方案的在线挑战问题的属性。结果表明，PEQUOD解决验证问题，不能解决目前的技术。
2019-07-09 cs.LO cs.PL
On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic
University of Bologna, Italy（博洛尼亚大学）；INRIA Sophia Antipolis, France（法国索菲亚安提佩利斯国家信息与自动化研究所）；Université Claude Bernard Lyon 1, France（法国里昂第一大学）
本文研究了概率高阶递归方案的终止问题，利用线性逻辑的加权关系语义将问题转化为生成函数的计算，证明了在扩展Li等人affine PHORS的类型纪律下，几乎必然终止的可判定性。
2026-04-30 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
Step-Indexed Relational Reasoning for Countable Nondeterminism
具有可数不确定性选择的程序设计语言在计算上是有趣的，因为可数不确定性在为并发系统的公平性建模时出现。由于可数选择引入了非连续行为，因此众所周知，为具有可数非确定性的程序设计语言开发语义模型是具有挑战性的。我们提出了一个步骤索引的逻辑关系模型的高阶函数程序设计语言可数不确定性，并演示了它如何可以用来推理上下文定义的可能和必须等价。在早期的阶跃指数模型中，指数是从ω中得出的。在这里，必须等价的步骤索引关系在大于ω的序数上索引。
2013-10-10 cs.LO
An asymptotic analysis of probabilistic logic programming, with implications for expressing projective families of distributions
LMU München（慕尼黑大学）
概率逻辑编程是统计关系型人工智能的重要组成部分，其中将逻辑和概率方法结合在一起，在不确定性环境中推理和学习关系域。然而，跨可变域大小的统计关系表示的行为是复杂的，并且将推理和学习扩展到大型域仍然是一个重大挑战。近年来，域大小依赖、提升推理和从抽样子群体中学习之间出现了联系。统计关系表示的渐近行为已经受到审查，和投影被调查的最强形式的域大小的依赖，其中查询边际是完全独立的域大小。在这篇文章中，我们证明了每一个概率逻辑程序下的分布语义是渐近等价于一个非循环的概率逻辑程序只包括确定条款的概率事实。我们的结论是，每一个概率逻辑程序诱导一个投影族的分布，实际上是处处等价于一个程序从这个片段，我们调查的后果，为投影族的分布概率逻辑程序表示。为了方便应用的经典结果从有限模型理论，我们引入了抽象的分布语义，定义为一个任意的逻辑理论概率事实。这弥合了与概率逻辑编程基础的分布语义之间的差距。在这种表示中，确定性逻辑程序对应于无量词理论，使得渐近量词消去结果可用于概率逻辑编程的设置。本文件正在考虑被TPLP接受。
2021-08-18 cs.AI cs.LO cs.PL
Coupled Relational Symbolic Execution for Differential Privacy
差分隐私是数据隐私的一个事实标准，在私营和公共部门都有应用。大多数实现差分隐私的技术都是基于对随机性的明智使用。然而，推理随机程序是困难的，容易出错。出于这个原因，最近已经提出了几种技术来支持设计师在证明程序的差异隐私或发现违规it.In这项工作中，我们提出了一种基于符号执行推理的技术差分隐私。符号执行是用于测试、反例生成和证明没有错误的经典技术。在这里，我们使用符号执行来支持这些任务，特别是差分隐私。为了实现这一目标，我们利用了两个已被证明在有关差分隐私的形式推理中有用的想法：关系推理和概率耦合。我们的技术集成了这两个想法，并展示了如何使用这样的组合来验证和发现违反差分隐私。
2020-07-25 cs.LO cs.PL
Compositional Vulnerability Detection with Insecurity Separation Logic (Extended Version)
本文提出下近似关系型程序逻辑 InsecSL，通过基于 bi-abduction 的符号执行支持交互式类 C 程序中内存安全与信息泄露的组合式、增量检测，并在两种实现上进行评估。
2023-08-21 cs.CR cs.LO cs.PL
Quantum Relational Hoare Logic
我们提出了一个逻辑的推理对互动的量子程序-量子关系霍尔逻辑（qRHL）。这种逻辑遵循概率关系霍尔逻辑（Barthe et al. 2009）的精神，并允许我们在给定输入关系的情况下，用公式表示两个量子程序的输出如何相关。概率RHL被广泛用于经典密码协议的计算机验证安全性证明。由于pRHL不适合分析量子密码，我们提出qRHL作为替代，适合后量子密码和量子协议的安全性分析。qRHL的设计对量子设置提出了一些独特的挑战，例如，量子寄存器上相等的定义。最后，我们实现了一个工具来验证qRHL中的证明，并在其中开发了几个示例安全证明。
2019-01-14 cs.LO quant-ph
An algebra of alignment for relational verification
关系验证包括信息流安全性、回归验证、编译器的转换验证等。程序和计算的有效对齐有助于使用更简单的关系不变量和关系过程规范，这反过来又使自动化和模块化推理成为可能。对齐已被探索的痕迹对，演绎规则的关系霍尔逻辑（RHL），和几种形式的产品自动机。本文展示了一个简单的扩展Kleene代数与测试（KAT），称为BiKAT，包含先前的公式，包括对齐证人forall-exists属性，这带来了新的RHL风格的规则，这些属性。对齐可以发现算法或手动设计，但在任何一种情况下，他们的充分性相对于原始程序必须证明;一个明确的代数使建设性的证明方程推理。此外，我们的方法继承了现有的基于KAT的技术和工具，这是适用于一系列的语义模型的算法的好处。
2023-03-23 cs.LO
A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic
本文提出在概率关系霍尔逻辑中直接证明惰性采样程序不可区分性的新方法，无需急切采样转换及相关假设，并在EasyCrypt中实现验证。
2023-11-28 cs.CR cs.FL cs.LO
Domain Reasoning in TopKAT
本文研究了TopKAT相对于关系模型的完备性，证明其对KAT项的（余）域比较完备，但对任意TopKAT项不完备，且该不完备性对欠近似规范推理影响有限。
2024-04-29 cs.LO cs.PL
Enhancing Predicate Pairing with Abstraction for Relational Verification
关系验证是一种旨在证明两个不同程序片段或两个不同程序运行相关属性的技术。它已被证明，受约束的霍恩子句（CHC）可以有效地用于关系验证，通过应用CHC转换，称为谓词配对，它允许CHC求解器推断不同谓词的参数之间的关系。在本文中，我们研究了如何通过使用基于线性算术的各种抽象域（即，凸多面体的域和它的一些子域）。在提出了一个算法与抽象谓词配对，我们报告的实验，我们已经进行了一百多个关系验证问题，通过使用各种抽象域。实验已经进行了使用VeriMAP转换和验证系统，连同帕尔马多面体库（PPL）和Z3求解器的CHCs。
2017-09-14 cs.LO cs.SE
Demonic Lattices and Semilattices in Relational Semigroups with Ordinary Composition
关系代数及其约简为非确定性程序及其部分正确性的推理提供了有力的工具。引入恶魔演算来模拟机器的行为，其中恶魔控制着非决定论，也为我们提供了完全正确的推理扩展。我们正式的框架，关系推理的总正确性，在不确定性程序使用半群与普通的组成和恶魔格操作。我们证明了可表示的恶魔并半群类是不可公理化的，恶魔交半群的表示类对于其有限成员不具有有限表示性质.对于格半群（具有复合、恶魔并和恶魔交），我们证明了有限代数的表示问题是不可判定的，而且有限表示问题也是不可判定的.由此可见，表示类是不可公理化的，而且有限表示性质也不成立。
2021-05-14 cs.LO math.LO
Making Relational Hoare Logic Alignment Complete
针对关系验证中的对齐完备性问题，提出基于带测试克林代数的语义保持重写规则，证明RHL相对于通用对齐自动机具有对齐完备性，打通了语法推理与自动机验证的壁垒。
2023-07-20 cs.LO
Minimally Comparing Relational Abstract Domains
针对抽象域逻辑蕴含比较中因携带效应导致不精确的问题，提出一种不动点算法将极小化变量包含到比较公式中，提升了比较粒度并有效减少了不可判定与不可比较的不变式数量。
2023-05-25 cs.LO
Relational reasoning via probabilistic coupling
概率耦合是分析概率过程对的有力工具。粗略地说，耦合两个过程需要找到一个合适的见证过程，在同一概率空间中对两个过程进行建模。耦合是证明两个过程之间关系的强大工具，包括关于分布收敛和随机优势的推理-单调性属性的概率版本。虽然耦合的数学定义看起来相当复杂和繁琐的操作，我们表明，关系程序逻辑pRHL-逻辑基础的EasyCrypt密码证明助手-已经内化的概率耦合的泛化。有了这种见解，构造耦合并不比构造逻辑证明难。我们演示了如何表达和验证pRHL耦合的经典例子，我们机械地验证了EasyCrypt中的几个耦合。
2015-10-14 cs.LO cs.PL
Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
Fondazione Bruno Kessler（布鲁诺·凯斯勒基金会）；Technische Universität Wien（维也纳工业大学）
处理上下文相关的知识导致了不同的形式化的概念的背景。其中之一是情境化知识库（CKR）框架，它植根于描述逻辑，但在推理方面与逻辑程序，特别是回答集编程（ASP）有很强的联系。CKR框架迎合了上下文中具有可废止公理和例外的推理，并将其扩展到覆盖（特异性）层次结构中的跨上下文知识继承。然而，该方法只支持这种单一类型的上下文关系和推理程序的工作仅限于层次结构，由于非平凡的问题与模型的偏好下的异常。在本文中，我们克服了这些限制，并提出了一个推广的CKR层次结构的多个上下文关系，以及他们的解释，可废止的公理和偏好。为了支持推理，我们使用ASP与代数措施，这是一个最近的扩展ASP加权公式半环，允许一个关联的数量与解释取决于命题原子的真值。值得注意的是，我们表明，CKR层次结构与多个上下文关系的相关片段，查询回答可以实现与流行的asprin框架。代数措施的方法是更强大的，并使例如推理与认知查询CKR，这打开了有趣的角度使用定量ASP扩展在其他应用程序。
2021-12-21 cs.AI cs.LO
Modal reduction principles across relational semantics
本文建立了系统的联系，一阶对应的Sahlqvist模态约简原则在各种关系的语义设置，其中包括脆和多值Kripke框架，脆和多值极性为基础的框架（又名丰富的形式背景）。建立在统一对应理论，我们的目标是引入一个理论环境，使之有可能：（a）比较和相互关联的各种框架对应（b）识别不同类型关系结构的框架对应语言中的一阶句子何时编码相同的“模态内容”;（c）在不同的语义语境中有意义地传递和表示众所周知的关系属性，如反身性、传递性、对称性、连续性、汇合性、密度。这些结果可以被理解为研究计划的第一步，该计划旨在使对应论不仅（方法上）统一，而且（有效地）参数化。
2023-02-13 cs.LO
Combining Relational Algebra, SQL, Constraint Modelling, and Local Search
本文的目标是提供一个强大的约束建模和关系数据库管理系统之间的集成。为此，我们建议扩展标准的查询语言，如关系代数和SQL，通过添加约束建模功能。特别是，我们提出了两种语言，这是特别适合于组合问题的非确定性扩展。非确定性是通过猜测算子引入的，它声明一组关系具有任意扩展。这个新的运算符导致语言具有更高的表达能力，能够表达复杂性类NP中的所有问题。给出了使数据复杂度多项式化的一些语法限制。这两个扩展的有效性证明了通过几个例子。目前的实现，用Java编写的本地搜索技术，描述。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2006-01-11 cs.AI cs.LO
