Two-Variable Separation Logic and Its Inner Circle

DOI10.1145/2724711zbMath1354.03036OpenAlexW2066800627MaRDI QIDQ2957697

Morgan Deters, Stéphane P. Demri

Publication date: 27 January 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2724711

Mathematics Subject Classification ID

Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25)

Related Items

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ Separation logics and modalities: a survey ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Unnamed Item ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ On Temporal and Separation Logics ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning

Uses Software

• Slide

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Maintaining knowledge about temporal intervals
• On the almighty wand
• Expressiveness and complexity of graph logic
• Complexity results for classes of quantificational formulas
• Undecidability results on two-variable logics
• A logical characterization of data languages.
• The complexity of propositional linear temporal logics in simple cases
• The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic
• Equality and monodic first-order temporal logic
• Two variable first-order logic over ordered domains
• Nondeterministic Phase Semantics and the Undecidability of Boolean BI
• Tractable Reasoning in a Fragment of Separation Logic
• Undecidability of Propositional Separation Logic and Its Neighbours
• Ordered Navigation on Multi-attributed Data Words
• ENTSCHEIDUNGSPROBLEM REDUCED TO THE AEA CASE
• A Modal BI Logic for Dynamic Resource Properties
• Beyond Shapes: Lists with Ordered Data
• A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time
• The modal logic of inequality
• Methods for Automated Theorem Proving in Nonclassical Logics
• On languages with two variables
• Undecidability of modal and intermediate first-order logics with two individual variables
• On the Decision Problem for Two-Variable First-Order Logic
• A decision procedure for satisfiability in separation logic with inductive predicates
• Decidability of weak logics with deterministic transitive closure
• The Tree Width of Separation Logic with Recursive Definitions
• Separation Logic with One Quantified Variable
• Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
• Complexity of Two-Variable Logic on Finite Trees
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Two-Variable Logic with Two Order Relations
• Two-Variable First-Order Logic with Equivalence Closure