Name
Title | ||
|---|---|---|
Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules |
Abstract | ||
|---|---|---|
Entailment is undecidable in general for Separation (SL) Logic formulæ 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. |
Year | DOI | Venue |
|---|---|---|
2022 | 10.1016/j.ipl.2021.106169 | Information Processing Letters |
Keywords | DocType | Volume |
Separation logic,Inductive definition,Decidability,Automatic theorem proving | Journal | 173 |
ISSN | Citations | PageRank |
0020-0190 | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mnacho Echenim | 1 | 95 | 15.75 |
| Radu Iosif | 2 | 483 | 42.44 |
| Nicolas Peltier | 3 | 50 | 11.84 |