Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules Article - Janvier 2022

Mnacho Echenim, Radu Iosif, Nicolas Peltier

Mnacho Echenim, Radu Iosif, Nicolas Peltier, « Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules  », Information Processing Letters, janvier 2022, p. 106169. ISSN 0020-0190

Abstract

Entailment is undecidable in general for Separation (SL) Logic formulae with inductive definitions, but it has been shown to be decidable [1] if the inductive rules satisfy three conditions, namely progress, connectivity and establishment. We show that entailment is undecidable if the latter condition is dropped, thus drawing a much clearer frontier for (un)decidability.

Voir la notice complète sur HAL

Actualités