A Complete Axiomatisation for Quantifier-Free Separation Logic
The work
| Title | A Complete Axiomatisation for Quantifier-Free Separation Logic |
|---|---|
| Authors | Stéphane Demri; Étienne Lozes; Alessio Mansutti |
| Type | article |
| Year | 2021 |
| Citekey | demri2021complete |
Where it appeared
| Published in | Logical Methods in Computer Science |
|---|---|
| Publisher | Logical Methods in Computer Science e.V. |
| Volume | Volume 17, Issue 3 |
Identifiers
| DOI | 10.46298/lmcs-17(3:17)2021 |
|---|---|
| OpenAlex | W3034779625 |
Access
| Landing page | https://doi.org/10.46298/lmcs-17(3:17)2021 |
|---|---|
| Free full text | https://lmcs.episciences.org/8347/pdf |
Abstract
We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the concrete semantics needs to be taken into account. Therefore, we present the first internal Hilbert-style axiomatisation for quantifier-free separation logic. The calculus is divided in three parts: the axiomatisation of core formulae where Boolean combinations of core formulae capture the expressivity of the whole logic, axioms and inference rules to simulate a bottom-up elimination of separating connectives, and finally structural axioms and inference rules from propositional calculus and Boolean BI with the magic wand.
Copy held
| Kind | PDF, 799.2 kB |
|---|---|
| Retrieved | 2026-08-05 |
| Held | local, for personal reference |
| Where it came from | https://lmcs.episciences.org/8347/pdf |
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Standing | endorsed |
| Approved | 2026-08-05 |
Cite it as
@article{demri2021complete,
title = {A Complete Axiomatisation for Quantifier-Free Separation Logic},
author = {Stéphane Demri and Étienne Lozes and Alessio Mansutti},
year = {2021},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
publisher = {Logical Methods in Computer Science e.V.},
doi = {10.46298/lmcs-17(3:17)2021},
url = {https://lmcs.episciences.org/8347/pdf},
}
This record lives at https://refs.drheap.org/demri2021complete/ and will keep doing so.