Unifying decidable entailments in separation logic with inductive definitions

DOI10.1007/978-3-030-79876-5_11OpenAlexW3183368753MaRDI QIDQ2055854

Nicolas Peltier, Radu Iosif, Mnacho Echenim

Publication date: 1 December 2021

Full work available at URL: https://arxiv.org/abs/2012.14361

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Foundations for entailment checking in quantitative separation logic ⋮ Unifying decidable entailments in separation logic with inductive definitions ⋮ Decision problems in a logic for reasoning about reconfigurable distributed systems ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

Cites Work

• Unifying decidable entailments in separation logic with inductive definitions
• Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
• Automated mutual induction proof in separation logic
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• The Tree Width of Separation Logic with Recursive Definitions
• The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates
• BI as an assertion language for mutable data structures
• Foundations for Decision Problems in Separation Logic with General Inductive Predicates

This page was built for publication: Unifying decidable entailments in separation logic with inductive definitions