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

DOI10.1016/J.IPL.2021.106169OpenAlexW3091716098MaRDI QIDQ2234797FDOQ2234797

Authors: Mnacho Echenim, Radu Iosif, Nicolas Peltier 

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

Recommendations

• scientific article; zbMATH DE number 2090860
• An undecidability result for separation logic with theory reasoning
• Unifying decidable entailments in separation logic with inductive definitions
• Undecidability of propositional separation logic and its neighbours
• The undecidability of entailment and relevant implication
• Disproving inductive entailments in separation logic via base pair approximation
• scientific article; zbMATH DE number 1256672
• scientific article; zbMATH DE number 1138201
• Non-deterministic logic of informal provability has no finite characterization
• Undecidability of the problem of recognizing axiomatizations for propositional calculi with implication

zbMATH Keywords

decidabilityseparation logicautomatic theorem provinginductive definition

Mathematics Subject Classification ID

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

Cites Work

• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• BI as an assertion language for mutable data structures
• The tree width of separation logic with recursive definitions

Cited In (1)

• Unifying decidable entailments in separation logic with inductive definitions

Uses Software

• Slide

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

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