Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules

DOI10.1016/j.ipl.2021.106169OpenAlexW3091716098MaRDI QIDQ2234797

Radu Iosif, Nicolas Peltier, Mnacho Echenim

Publication date: 19 October 2021

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2021.106169

zbMATH Keywords

decidabilityseparation logicautomatic theorem provinginductive definition

Mathematics Subject Classification ID

Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (1)

Unifying decidable entailments in separation logic with inductive definitions

Uses Software

• Slide

Cites Work

• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• The Tree Width of Separation Logic with Recursive Definitions
• BI as an assertion language for mutable data structures

This page was built for publication: Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules