Two-Variable Separation Logic and Its Inner Circle

DOI10.1145/2724711MaRDI QIDQ2957697zbMATH OpenOpenAlexWikidataFDO

Authors Stéphane Demri, Morgan Deters

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

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

Recommendations

• On logics with two variables
• Semipositivity in separation logic with two variables
• Two-variable logic on 2-dimensional structures
• The Two-Valued Iterative Systems of Mathematical Logic. (AM-5)
• scientific article; zbMATH DE number 1078559
• Two-variable first-order logic with equivalence closure
• Two-variable first-order logic with equivalence closure
• Two-variable logic with two order relations
• Expressive completeness of separation logic with two variables and no separating conjunction
• Expressive completeness of separation logic with two variables and no separating conjunction

Cites work

• \(\mathrm{FO}^2\) with one transitive relation is decidable
• A decision procedure for satisfiability in separation logic with inductive predicates
• A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time
• A logical characterization of data languages.
• A modal BI logic for dynamic resource properties
• Beyond Shapes: Lists with Ordered Data
• Complexity of two-variable logic on finite trees
• Complexity results for classes of quantificational formulas
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Decidability of weak logics with deterministic transitive closure
• ENTSCHEIDUNGSPROBLEM REDUCED TO THE AEA CASE
• Equality and monodic first-order temporal logic
• Expressive completeness of separation logic with two variables and no separating conjunction
• Expressiveness and complexity of graph logic
• scientific article; zbMATH DE number 3827831 (Why is no real title available?)
• scientific article; zbMATH DE number 3688686 (Why is no real title available?)
• scientific article; zbMATH DE number 1989660 (Why is no real title available?)
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1852922 (Why is no real title available?)
• scientific article; zbMATH DE number 3271460 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• Maintaining knowledge about temporal intervals
• Methods for Automated Theorem Proving in Nonclassical Logics
• Modal logic
• Nondeterministic phase semantics and the undecidability of Boolean BI
• On languages with two variables
• On the almighty wand
• On the Decision Problem for Two-Variable First-Order Logic
• Ordered navigation on multi-attributed data words
• Separation logic with one quantified variable
• 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
• The modal logic of inequality
• The tree width of separation logic with recursive definitions
• Tractable Reasoning in a Fragment of Separation Logic
• Two variable first-order logic over ordered domains
• Two-variable first-order logic with equivalence closure
• Two-variable logic with two order relations
• Undecidability of modal and intermediate first-order logics with two individual variables
• Undecidability of propositional separation logic and its neighbours
• Undecidability results on two-variable logics

Cited in

(16)

• Semipositivity in separation logic with two variables
• The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Undecidability of propositional separation logic and its neighbours
• On the almighty wand
• Separation logics and modalities: a survey
• Expressive completeness of separation logic with two variables and no separating conjunction
• QUESTIONS IN TWO-DIMENSIONAL LOGIC
• On temporal and separation logics
• Extending propositional separation logic for robustness properties
• The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
• Expressive completeness of separation logic with two variables and no separating conjunction
• The Two-Valued Iterative Systems of Mathematical Logic. (AM-5)
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• An algebraic glimpse at bunched implications and separation logic

Describes a project that uses

Uses Software

• Slide

This page was built for publication: Two-Variable Separation Logic and Its Inner Circle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2957697)