Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
本文研究分离逻辑中带归纳定义谓词的蕴涵问题，针对P规则和loc-deterministic归纳规则片段给出多项式时间的可靠完备循环证明过程，并证明条件放宽后问题不可处理。
2025-07-11 cs.LO
Enhancing Inductive Entailment Proofs in Separation Logic with Lemma Synthesis
提出了一种基于分离逻辑的引理综合方法，以支持高级归纳蕴涵过程。我们首先提出了一个引理自动证明和系统应用的机制。引理可以包括通用保护和/或未知谓词。虽然前者对于表达性至关重要，但后者对于支持多个谓词之间的关系至关重要。我们进一步引入引理合成来支持（i）自动归纳推理与框架推理以及（ii）定理探索。对于（i）我们在归纳证明过程中自动发现并证明辅助引理;对于（ii）我们自动生成一组有用的引理来关联用户定义或系统生成的谓词。我们已经实现了我们提出的方法到现有的验证系统，并测试其在归纳推理和定理探索的能力。实验结果表明，增强的系统可以自动合成有用的引理，以促进推理的广泛的非平凡归纳证明。
2018-05-12 cs.LO cs.PL
First Degree Entailment with Group Attitudes and Information Updates
我们扩展了认知逻辑与德摩根否定费金等人。内特尔79，203-240，1995），通过在一组代理中添加用于通用和公共知识的运算符，并使用非关联Lambek演算的左除法连接符的广义版本来形式化信息更新。我们提供了健全和完整的公理化的基本逻辑与群运算符和基本逻辑与群运算符和更新。这两个逻辑都被证明是可判定的。
2019-09-25 cs.LO
An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
一个有效的蕴涵证明系统对于使用分离逻辑的组合验证是必不可少的。不幸的是，现有的决策程序要么缺乏表达能力，要么效率低下。例如，Smallfoot是一个有效的过程，但只适用于硬连接的列表和树。其他可以支持一般归纳谓词的过程在时间上呈指数级运行，因为它们的证明搜索需要回溯来处理结果中的析取。本文给出了一个在多项式时间内推导一般归纳谓词循环蕴涵证明的判定过程。我们的程序是高效的，不需要回溯;它使用规范化规则，有助于避免在后果中引入析取。此外，我们的可判定片段是足够的表达：它是基于组合谓词，可以捕获广泛的数据结构，包括排序和嵌套的列表段，跳跃列表与快速前进指针，和二叉搜索树。我们已经实现了一个原型工具的建议，并评估它的挑战性问题，从最近的分离逻辑竞争。实验结果证实了所提出的系统的效率。
2022-10-02 cs.LO
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning
本文提出了一种基于逻辑演算的证明方法，结合归纳定义的谓词表示的有界树宽结构和理论推理，检验分离逻辑公式之间蕴涵的有效性。微积分是可靠的和完备的，在这个意义上，证明树是有效的当且仅当它允许一个（可能是无限的）证明树。我们表明，该过程在以下两种情况下终止：（i）当归纳规则，定义谓词发生在左手边的蕴涵终止，在这种情况下，证明树总是有限的。(ii)当理论是空的，在这种情况下，每个有效的证明树都允许一个有理证明树，其中在证明树中出现的成对不同序列的总数是关于r.t.的双指数。最后的结局。
2022-06-22 cs.LO
Completeness of Cyclic Proofs for Symbolic Heaps
分离逻辑在理论和实践上都是成功的软件验证方法。符号堆的判定过程是其中的关键问题之一。本文提出了一个具有一般形式归纳定义的符号堆循环证明系统，并证明了它的可靠性和完备性。最后给出了具有归纳定义的符号堆蕴涵的判定过程。具有归纳定义的符号堆的蕴涵的判定性是一个重要的问题。循环证明系统的完备性也是一个重要的问题。本文的结果回答了这两个问题。该判决过程是可行的，因为它是不确定的双指数时间复杂度。
2018-05-28 cs.LO
Query-Based Entailment and Inseparability for ALC Ontologies (Full Version)
我们调查的问题是否两个ALC知识库是不可区分的查询在一个给定的词汇。我们给模型理论的标准（部分）同态和产品，并证明了这个问题是不可判定的合取查询（CQ），但2 EXPTIME-完全的UCQ（工会的CQ）。如果CQ被根CQ替换，则同样的结果成立。我们还考虑的问题是否两个ALC TBox给出相同的答案，在一个给定的词汇表中的任何查询所有的ABoxes，并表明，对于CQ这个问题是不可判定的，太，但成为可判定的和2 EXPTIME-完全的霍恩-ALC，甚至EXPTIME-完全的霍恩-ALC时，限制（工会）根CQ。
2016-08-04 cs.LO
Rational fuzzy attribute logic
我们提出了一个逻辑推理的if-then公式，其中涉及常数的合理的真度从单位区间。我们引入了公式的分级语义和句法蕴涵。我们证明了该逻辑是Pavelka风格的完备逻辑，并且根据真度结构的选择，该逻辑是RationalPavelka逻辑（RPL）或RationalProductLogic（RPL）的可判定片段。我们还提出了一个基于最小模型的蕴涵的特征，并研究了相关的闭包结构。
2015-02-25 cs.LO
Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
我们开发了一个理论的可判定的归纳不变量的无限状态变量的应用π演算，与应用程序的自动验证有状态的加密协议与无界会话/随机数。由于这个问题是不可判定的一般，我们引入深度有界的协议，严格概括的一类文献，我们的可判定分析是健全和完整的。我们的核心贡献是一个检查不变量是归纳的过程，这意味着每个可达配置满足它。我们的不变量可以捕获安全属性，如保密性，可以自动推断，并表示一个独立的可检查的正确性证书。我们提供了一个原型实现，我们报告其性能的一些教科书的例子。
2020-07-19 cs.CR cs.FL cs.LO
Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints
我们确定差异约束集约束（DBS），一个类比的差异约束算术约束集。DBS不仅可以表示集合约束，而且可以表示集合元素上的算术约束。我们将DBS集成到具有线性组合归纳谓词的分离逻辑中，获得其中可以指定线性数据结构的集合数据约束的逻辑。我们证明了这个逻辑的可满足性是可判定的。决策过程的一个关键步骤是计算DBS可定义的集合关系的传递闭包，为了捕获它，我们提出了一种扩展的量化集合约束与Presburger算术（RQSPA）。RQSPA的可满足性，然后证明是可判定的利用先进的自动机理论技术。
2018-11-02 cs.LO
Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
本文研究允许归纳定义内含指针算术的分离逻辑片段 SLAH，通过归纳定义摘要的线性化及空间原子匹配切分，给出可满足性与蕴含判定过程，并在内存分配器验证任务上验证性能。
2024-03-04 cs.LO
Two Results on Separation Logic With Theory Reasoning
本文给出了关于谓词符号为归纳定义的分离逻辑和理论推理中蕴涵问题的两个结果。首先，我们证明了在理论推理的情况下，对于树宽有界的规则，蕴涵问题是不可判定的。这一结果适用于许多理论，即使它们的表达能力很低。例如，它适用于具有后继函数或具有通常顺序的自然数。其次，我们证明了每个蕴涵问题都可以归结为一个蕴涵问题，不包含平等（无论是在公式中，也不是在递归规则定义的谓词符号的语义）。
2022-06-19 cs.LO
Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying
Technische Universität Dresden（德累斯顿工业大学）
在我们追求的通用标准，可判定的基于本体的查询，我们引入“有限宽度集”（FCS）的存在规则，模型理论上定义的一类规则集，灵感来自图论的宽度测量。通过一个通用的参数，我们表明，FCS确保了一个相当大的类的查询（称为“DaMSOQs”）包含合取查询（CQ）的蕴涵的可判定性。FCS类适当地推广了有限扩展集（FES）类，并且对于arity至多为2的签名，推广了有界树宽集（BTS）类。对于更高层次，BTS只是通过具体化的方式间接地被FCS所包含。尽管FCS的一般性，我们提供了一个规则集与可判定CQ蕴涵（凭借一阶重写），落在FCS之外，从而证明了FCS和类的有限统一集（FUS）的不可比性。尽管如此，我们表明，如果我们限制自己的单头规则集的签名的arity最多为2，然后FCS归入FUS。
2022-09-06 cs.AI cs.DB cs.DM
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
分离逻辑的符号堆片段已被积极开发和提倡用于验证计算机程序的存储器安全性质。目前，其最大的挑战之一是有效地证明包含归纳堆谓词的蕴涵。这些蕴涵通常是在验证操作复杂数据结构（如链表、树或图）的程序时生成的证明义务。为了帮助证明这样的蕴涵，本文介绍了一个引理合成框架，自动发现引理，作为尤里卡步骤的证明。数学归纳法和基于模板的约束求解是我们框架的两大支柱。为了导出给定蕴涵的支持引理，框架首先从蕴涵的堆结构中识别可能的引理模板。然后，它建立每个模板的变量之间的未知关系，并进行结构归纳证明，以产生这些关系的约束。最后求解约束条件，找出未知关系的实际定义，从而发现引理。我们已经将这个框架集成到一个原型证明器中，并在各种蕴涵基准上进行了实验。实验结果表明，我们的引理合成辅助证明器可以证明许多蕴涵，不能处理现有的技术。这个新提议为自动推理复杂的归纳堆谓词提供了更多的机会。
2017-11-08 cs.LO cs.PL
The Tree Width of Separation Logic with Recursive Definitions
分离逻辑是一种广泛使用的形式主义，用于描述动态分配的链接数据结构，如列表，树等的逻辑的各个片段的可判定性状态构成了一个长期存在的开放问题。目前的结果报告的技术，以确定满足性和有效性的蕴涵分离逻辑（S）的列表（可能与数据）。在本文中，我们建立了一个更一般的可判定性结果。我们证明了任何使用较一般的递归定义谓词的分离逻辑公式都是可判定的可满足性，而且这些公式之间的蕴涵也是可判定的有效性.这些谓词足够通用，可以定义（双）链表、树和比树更通用的结构，比如叶子被链接在一个链表中的树。可判定性证明是通过将一元二阶逻辑在有界树宽度的图上的可判定性归约来实现的。
2013-03-30 cs.FL cs.LO
Logic of temporal attribute implications
Palacky University Olomouc（奥洛穆茨帕拉茨基大学）
我们研究逻辑推理与if-then公式描述对象的属性之间的依赖关系，观察在连续的时间点。我们介绍了语义蕴涵的公式，显示其不动点特征，调查封闭性质的模型类，提出了一个公理化，并证明其完整性，并调查替代公理化和规范化的证明。我们研究了逻辑的可判定性和复杂性问题，并证明了蕴涵问题是NP-难的，属于EXPSPACE。我们表明，通过限制到预测公式，蕴涵问题是可判定的伪线性时间。
2015-05-04 cs.AI cs.DB cs.LO
Preprocessing in Inductive Logic Programming
Linacre College University of Oxford（牛津大学李纳克尔学院）
归纳逻辑程序设计是一种机器学习，其中逻辑程序从示例中学习。这种学习通常相对于作为逻辑程序提供的某些背景知识发生。本文介绍了底层预处理，一种在ILP系统必须考虑的程序上生成初始约束的方法。底层预处理将逆蕴涵的思想应用于现代ILP系统。逆蕴涵是Progol引入的一种有影响力的早期ILP方法。本文还提出了$\bot$ -Popper，它是现代ILP系统Popper的底层预处理的一个实现.实验表明，底层预处理可以减少ILP系统在困难问题上的学习时间。当问题中的背景知识量很大时，这种减少可能特别显著。
2021-12-21 cs.AI cs.LG cs.LO
Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems
我们考虑一个逻辑用于描述分布式系统的配置集，其网络拓扑结构可以在运行时改变，由重新配置程序。该逻辑使用归纳定义来描述具有无限数量的组件和交互的网络，使用乘法合取来编写，让人想起集束蕴涵和分离逻辑。我们研究了配置逻辑的可满足性和蕴涵问题的复杂性。此外，我们还考虑了鲁棒性属性，例如紧密性（所有交互都与组件完全连接吗？）和度有界性（每个分量都参与有限数量的相互作用吗？），后者是蕴涵的可判定性的成分。
2022-04-26 cs.LO
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
本文研究了分离逻辑中证明机制的不完整性来源，并通过弱分离逻辑的完整性和非标准模型分析，揭示了证明失败的原因。
2025-12-04 cs.LO cs.PL
Derivation-Graph-Based Characterizations of Decidable Existential Rule Sets
TU Dresden（德累斯顿工业大学）
该研究基于推导图概念定义（弱）无环推导图集，通过证明论论证证明其与（弱）贪婪有界树宽集等价，为可判定存在规则集提供了新刻画，深化了相关证明论理解。
2023-07-18 cs.AI cs.DB cs.LO
Query Answering over Contextualized RDF/OWL Knowledge with Forall-Existential Bridge Rules: Decidable Finite Extension Classes (Post Print)
FBK-IRST（布鲁诺·凯斯勒基金会研究院）；University Of Trento（特伦托大学）；Otto-von-Guericke University of Magdeburg（马格德堡奥托·冯·格里克大学）
语义Web（SW）中上下文化知识的激增导致了诸如\emph{quads}之类的知识格式在SW社区中的流行。quad是RDF三元组的扩展，包含三元组的上下文信息。在本文中，我们研究的问题，查询回答四倍增加forall存在的桥规则，使在各种情况下的三元组之间的推理的互操作性。我们称一组四边形与这样的表达桥规则，一个四边形系统。一般来说，四系统上的查询应答是不可判定的。我们推导出可判定类的四系统，查询回答可以使用正向链接。健全的，完整的和终止的程序，这是众所周知的追逐算法的适应，提供这些类决定查询蕴涵。安全，msafe，和csafe类的四系统限制的追逐计算过程中产生的空白节点的结构有界深度的有向无环图（DAG）。RR和受限RR类不允许在追踪计算过程中生成空节点。数据和组合的复杂性的查询蕴涵已建立派生类。我们进一步表明，四系统是等价的forall存在的规则，其谓词被限制到三进制，模多项式时间的翻译。我们随后表明，安全技术严格包含在表达性中，一些众所周知的表达性技术，例如联合非循环性和模型忠实非循环性，用于在普遍存在规则领域中的可判定性保证。
2015-12-12 cs.AI cs.DB cs.LO
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
向量加法系统的可达性问题是网理论的一个中心问题。一般的问题是已知的，是可判定的算法完全基于经典的Komaju-Lambert-Mayr-Sacerdote-Tenney分解。本文使用这种分解来证明VAS识别的语言的Parikh图像是半伪线性的;一类扩展半线性集的类，a.k.a.在Presburger算术中可定义的集合。我们提供了一个应用程序，这个结果，我们证明了最终配置是不可到达的初始一个当且仅当存在一个半线性归纳不变，包含初始配置，但不是最终的。由于我们可以决定是否Presburger公式表示归纳不变量，我们推断存在不可达性的可检查证书。特别是，存在一个简单的算法来决定一般的VAS可达性问题的基础上两个半算法。第一个试图证明的可达性列举有限序列的行动和第二个试图证明的不可达列举Presburger公式。
2010-09-09 cs.LO
HORPO with Computability Closure : A Reconstruction
本文给出了高阶递归路径序的一个新的、可判定的定义，其中只在需要时进行类型比较，从而消除了对可计算性闭包的需要，并且显式地处理了约束变量，使得处理任意严格正归纳类型的递归成为可能.
2007-08-27 cs.LO
Biabduction (and Related Problems) in Array Separation Logic
我们研究数组分离逻辑（ASL），符号堆分离逻辑的变体，其中数据结构是指针或数组，即，分配的内存的连续块。这种逻辑为命令式数组程序的组合内存安全性证明提供了一种语言。我们专注于这个逻辑，这已被确立为在工业规模的自动规范推理的关键的双外展问题。我们提出了一个NP决策过程中产生的解决方案的合理质量的ASL，双绑架，我们还表明，找到一个一致的解决方案的问题是NP-困难的。一路上，我们研究可满足性和蕴涵在我们的逻辑，决策程序和复杂性界的两个问题。我们证明了可满足性是NP完全的，并且蕴含着高复杂度的可判定性。有点令人惊讶的事实，即双绑架是比蕴涵简单得多的解释的事实，因为我们表明，双绑架解决方案的选择元素，使我们能够大大减少搜索空间。
2016-11-18 cs.DS cs.LO cs.PL
A Calculus of Apartness over Separoids: Effective Convex Representation, Stratified Conservativity, and the Complexity of Entailment
Bahcesehir University（巴切希尔大学）
研究有限族紧凸体诱导的相离关系，提出有效有理实现定理，证明布尔蕴含的完备性与可判定性，并分析计算复杂性。
2026-06-12 cs.CG cs.LO
Data Complexity in Expressive Description Logics With Path Expressions
TU Dresden（德累斯顿工业大学）；University of Wrocław（弗罗茨瓦夫大学）
本文分析 ZOIQ 在拟森林上可满足性的数据复杂性，证明其 NP 完全，并据此重新刻画 OWL2 SR 族及 ZIQ 根查询蕴涵的复杂性界限。
2024-06-11 cs.AI cs.CC cs.LO
Chase Termination Beyond Polynomial Time
本文提出允许部分循环的新追算终止判据，得到表达力更强且可判定复杂度达任意k-ExpTime的tgds片段，并进一步细化条件以在PSpace或k-ExpSpace中判定查询蕴含。
2024-03-28 cs.DB cs.LO
On the Expressiveness of a Logic of Separated Relations
我们比较模型理论的表达性的存在片段的分离逻辑在不受限制的关系签名（SLR）-只有分离的连接作为逻辑连接和高阶归纳定义，传统上称为符号堆片段-与（一元）二阶逻辑（（M）SO）的表达性。虽然SLR和MSO在无限树宽的结构上是不可比的，但事实证明，SLR可以嵌入SO中，一般来说，当模型的树宽由作为输入的参数限制时，MSO成为SLR的严格子集。我们还讨论了定义一个片段的SLR，相当于MSO模型的有界树宽的问题。这样的片段，然后将成为最一般的分离逻辑与可判定的蕴涵问题，一个关键成分的实际验证方法的自适应（可重构）组件为基础的和分布式系统。
2022-08-02 cs.LO
Decidability of Querying First-Order Theories via Countermodels of Finite Width
Technische Universität Dresden（德累斯顿工业大学）
提出基于有限宽度反模型的通用框架证明逻辑蕴含问题可判定性，采用partitionwidth度量，以存在规则为例展示其涵盖已知可判定类与新规则集，并揭示有限统一集的局限与补救方案。
2025-04-21 cs.AI cs.DB cs.DM
Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations
本文研究关系分离逻辑SLR的MSO可定义性，提出一个可描述有界树宽图集合并能有效翻译为MSO的表达性片段，从而保证可满足性与蕴含问题的可判定性。
2024-02-25 cs.FL cs.LO
On an Invariance Problem for Parameterized Concurrent Systems
我们认为并发系统由复制的有限状态进程，通过联合互动与用户定义的拓扑结构的网络中同步。该系统使用具有乘法连接词和归纳定义的谓词的资源逻辑来指定，让人想起分离逻辑。我们考虑的问题是，如果在这个逻辑中给定的公式定义了一个不变量，即公式的任何模型，遵循任意的相互作用激发序列，是否被转换为同一公式的另一个模型。这个属性，称为\emph{havoc invariance}，是证明在运行时改变网络结构的重新配置程序的正确性的精髓。我们发现，破坏不变性问题是多-一约化的蕴涵问题$ϕ\models ψ$，询问如果任何模型的$ϕ$也是一个模型的$ψ$。虽然，在一般情况下，浩劫不变性被发现是不可判定的，这种减少允许证明，浩劫不变性是在2 EXP，一般片段的逻辑，与2 EXP蕴涵问题。
2022-04-26 cs.DC cs.LO
Strong-Separation Logic
大多数分离逻辑的自动验证器都以符号堆碎片为目标，不允许魔术棒运算符和经典布尔运算符应用于空间公式。这并不奇怪，因为对魔杖的支持很快导致了不可判定性，特别是当与归纳谓词结合用于数据结构的推理时。为了规避这些不可判定性的结果，我们建议分配一个更严格的语义分离合取。我们认为，由此产生的逻辑，强分离逻辑，可用于组合程序验证和双溯静态分析就像“标准”的分离逻辑，同时保持可判定的，即使在魔术棒和列表段谓词的存在下-功能的组合，导致undecidability假设标准的语义。
2021-03-11 cs.LO
A Logic of Reachable Patterns in Linked Data-Structures
我们定义了一个新的可判定的逻辑表达和检查不变量的程序，操纵动态分配的对象，通过指针和破坏性的指针更新。这种逻辑的主要特点是能够限制从指定节点通过正则表达式可到达的节点的邻域。该逻辑在布尔运算（蕴涵、否定）下是封闭的，并且具有有限模型属性。关键的技术成果是可判定性的证明。我们展示了如何表达一些有趣的程序的前提条件，后置条件和循环不变式。也可以表示诸如数据结构的不相交性和低级堆变化之类的属性。此外，我们的逻辑可以表示任意数据结构和任意数量的指针字段的属性。后者提供了一种自然地指定后置条件的方法，后置条件将过程入口处的字段与出口处的字段联系起来。因此，可以使用该逻辑来自动证明执行低级堆突变的程序的部分正确性。
2007-05-24 cs.LO
$Π_{2}$-Rule Systems and Inductive Classes of Gödel Algebras
提出直觉主义和模态逻辑的一般 $Π_{2}$-规则理论，引入规则系统和归纳类概念，分析 Gödel 代数归纳类结构，证明存在连续统多个扩展 LC 的规则系统，并解决 LC 中可容许性的分类与可判定性问题。
2024-11-13 cs.LO math.LO
Query Answering with Transitive and Linear-Ordered Data
我们考虑蕴涵问题，涉及强大的约束语言，如守卫存在的规则，其中额外的语义限制放在一组杰出的关系。我们考虑限制一个关系是传递的，限制一个关系是另一个关系的传递闭包，限制一个关系是线性序。我们给出了一些自然的概括的guardedness，允许推断在每种情况下是可判定的，并隔离相应的决策问题的复杂性。最后，我们表明，轻微的变化，我们的条件导致不可判定性。
2016-07-04 cs.DB cs.LO
Paxos Made EPR: Decidable Reasoning about Distributed Protocols
Paxos等分布式协议在许多计算机系统中起着重要的作用。因此，分布式协议中的错误可能会产生巨大的影响。因此，在核查此类协议方面投入了大量努力。然而，检查这些协议的不变量是不可判定的，在实践中很难，因为它需要对无限数量的节点和消息进行推理。此外，协议动作和不变量涉及量词交替和高阶概念，如集合基数和算术。本文朝着此类协议的自动验证迈出了一步。我们的目标是一种技术，可以验证正确的协议，并识别错误的协议。为此，我们开发了一种基于有效命题逻辑（EPR）的演绎验证方法-一阶逻辑（也称为Bernays-Schönfinkel-Ramsey类）的可判定片段。除了可判定性，EPR还具有有限模型属性，允许将违规显示为用户直观的有限结构。我们的方法涉及使用一般（未解释）的一阶逻辑建模协议，然后系统地转换模型，以获得一个模型和一个可判定的归纳不变量检查。转换的步骤也被机械地检查，以确保方法的可靠性。我们已经使用我们的方法来验证Paxos及其几个变体的安全性，包括Multi-Paxos，Vertical Paxos，Fast Paxos，Flexible Paxos和Stoppable Paxos。据我们所知，这项工作是第一个使用可判定逻辑来验证这些协议，并且是第一个对垂直Paxos，快速Paxos和可停止Paxos的形式化验证。
2017-10-19 cs.DC cs.LO cs.PL
Living Without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions
本文针对含名词和角色包含的描述/模态逻辑不具备CIP与PBDP的问题，证明插值元与显式定义存在性仍可判定，明确不同场景下的复杂度，并给出适用于含角色包含描述逻辑的计算算法。
2023-04-28 cs.LO
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
我们介绍堆自动机，一个形式主义的符号堆碎片的分离逻辑与用户定义的归纳谓词的鲁棒性自动推理。可满足性、可达性和非循环性等鲁棒性属性对于基于分离逻辑的自动程序分析和验证中的各种推理任务都很重要。以前，这样的性质已经出现在分离逻辑文献的许多地方，但没有被系统地研究。在本文中，我们开发了一个基于堆自动机的算法框架，使我们能够以统一的方式获得广泛的鲁棒性的渐近最优决策程序。我们实现了我们的框架的原型，并取得了可喜的成果，所有上述的鲁棒性。此外，我们证明了堆自动机的适用性超出了鲁棒性。我们应用我们的算法框架的模型检验和蕴涵问题的符号堆分离逻辑。
2016-10-22 cs.LO
Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic
分离逻辑（SL）是一种众所周知的断言语言，用于具有动态分配的数据结构的程序的霍尔式模块化证明系统中。在本文中，我们研究的片段限制到Bernays-Schoenfinkel-Ramsey量词前缀$\exists^*\forall^*$，其中的量化变量的范围内的一组内存位置的一阶SL。当这个集合是未解释的（没有相关的理论）时，片段是PSPACE完备的，这与无量词片段的复杂性相匹配。然而，当量词前缀属于$\exists^*\forall^*\exists^*$时，或者当存储器位置被解释为具有线性算术约束的整数时，SL变得不可判定，从而为SL内的可判定性设置了清晰的边界。我们已经实现了一个决策程序的可判定片段的$\exists^*\forall^*$ SL作为一个专门的求解器内的DPLL（$T$）架构，在CVC 4 SMT求解器。我们的实现进行了评估，使用两组验证条件，产生（i）展开归纳谓词，和（ii）最弱的基于前置条件的验证条件生成器。实验数据表明，自动化的量词实例化具有很小的开销相比，手动基于模型的实例化。
2016-11-23 cs.LO
Quantified Constraints and Containment Problems
量化约束满足问题$\mathrm{QCSP}(\mathcal{A})$是判定仅涉及两个量词和连词的正Horn句子在某个固定结构$\mathcal{A}$上是否为真的问题。我们研究了两个与QCSP相关的包容问题。首先，我们给出了有限结构$\mathcal{A}$和$\mathcal{B}$的一个组合条件，该条件是生成$\mathrm{QCSP}(\mathcal{A}) \subseteq \mathrm{QCSP}(\mathcal{B})$的充分必要条件。证明了$\mathrm{QCSP}(\mathcal{A}) \subseteq \mathrm{QCSP}(\mathcal{B})$，即在$\mathcal{A}$上为真的正Horn逻辑的所有语句在$\mathcal{B}$上也为真，当且仅当存在从$\mathcal{A}^{|A|^{|B|}}$到$\mathcal{B}$的满射同态.这可以看作是改进了Keisler的一个旧结果，该结果表明前者等价于存在从$\mathcal{A}^ω$到$\mathcal{B}$的满射同态。我们注意到，该条件已经是保证包含QCSP的$Π_2$限制的必要条件，即$Π_2$ - $\mathrm{CSP}(\mathcal{A}) \subseteq Π_2$ - $\mathrm{CSP}(\mathcal{B})$。${|A|^{|B|}…
2015-09-10 cs.LO
Query Answering with Transitive and Linear-Ordered Data
Télécom ParisTech（巴黎高等电信学院）；Université Paris-Saclay（巴黎萨克雷大学）；University of Oxford（牛津大学）；CNRS（法国国家科学研究中心）；Université Lille 1（里尔第一大学）；INRIA Lille（法国国家信息与自动化研究所里尔分部）
我们认为蕴涵问题涉及强大的约束语言，如边境守卫的存在规则，我们施加额外的语义限制一组杰出的关系。我们考虑限制一个关系是传递的，限制一个关系是另一个关系的传递闭包，限制一个关系是线性序。我们给出了一些自然的变体的guardedness，使推理在每种情况下是可判定的，并隔离相应的决策问题的复杂性。最后，我们表明，在这些条件的轻微变化导致不可判定性。
2022-02-17 cs.AI cs.DB cs.LO
Bounded Model Checking of Pointer Programs Revisited
指针程序的有界模型检验是一种调试技术，用于操作堆上动态分配的指针结构的程序。它基于以下四点意见。第一，错误条件（如悬空指针的解引用）可以用双变量一阶逻辑的~片段来表示。其次，片段在最弱的前提条件wrt下是封闭的。有限路径第三，数据结构，如树、列表等，可以通过在数据库片段中定义的归纳谓词来表达。最后，双变量逻辑和数据库的两个片段的组合是可判定的。在本文中，我们通过扩展底层逻辑的表达能力来改进这种技术。在~序列的例子中，我们证明了新的逻辑是能够建模更复杂的数据结构与更复杂的依赖堆和更复杂的分析。
2016-02-29 cs.LO cs.PL
Derivatives for Containers in Univalent Foundations
Tallinn University of Technology（塔尔图理工大学）
本文在单子范畴中扩展了容器导数的概念，证明其在非截断容器中的普遍性质，并探讨了链式法则的可逆性问题。
2026-10-16 cs.LO
Verification of Component-based Systems with Recursive Architectures
研究了参数化构件系统的可靠性验证方法。该方法使用了资源逻辑，一种新的正式规约语言的分布式系统组成的一个有限的，但无界数量的组件。该逻辑允许通过与用于描述代数数据类型或递归数据结构的归纳定义类似的归纳定义来描述协调有限数量类型的组件的实例的架构配置。对于这种逻辑中指定的参数系统，我们表明，决策问题，如达到死锁或违反临界区是不可判定的，在一般情况下。尽管这个负面的结果，我们提供了这些决策问题的实际半算法依赖于自动合成的结构不变允许一般的安全性能的证明。使用一元二阶逻辑的WSkS片段定义不变量，已知其可由经典自动机逻辑连接判定，从而将验证问题减少到检查WSkS公式的可满足性。
2021-12-15 cs.FL cs.LO
