Entailment checking in separation logic with inductive definitions is 2-ExpTime hard

DOI10.29007/F5WHMaRDI QIDQ7024209zbMATH OpenFDO

Authors Mnacho Echenim, Radu Iosif, Nicolas Peltier

Publication date 20 February 2025

Full work available at URL https://doi.org/10.29007/F5WH

zbMATH Keywords

alternating Turing machinescomplexityinductionseparation logic

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25)

Cites work

• A decision procedure for satisfiability in separation logic with inductive predicates
• Alternation
• Deciding entailments in inductive separation logic with tree automata
• Effective entailment checking for separation logic with inductive definitions
• Foundations for decision problems in separation logic with general inductive predicates
• The Logic of Bunched Implications
• The tree width of separation logic with recursive definitions
• Unified reasoning about robustness properties of symbolic-heap separation logic

Cited in

(6)

• Decidable entailments in separation logic with inductive definitions: beyond establishment
• Tractable and intractable entailment problems in separation logic with inductively defined predicates
• A direct procedure to test entailment in a separation logic of relations
• Tree-verifiable graph grammars
• What is decidable in separation logic beyond progress, connectivity and establishment?
• An EXPTIME-complete entailment problem in separation logic

This page was built for publication: Entailment checking in separation logic with inductive definitions is 2-ExpTime hard

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