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

• 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?)
• A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time
• A decision procedure for satisfiability in separation logic with inductive predicates
• 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
• 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 Decision Problem for Two-Variable First-Order Logic
• On the almighty wand
• 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
• \(\mathrm{FO}^2\) with one transitive relation is decidable

Cited in

(16)

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

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)