Stéphane Demri ; Étienne Lozes ; Alessio Mansutti - A Complete Axiomatisation for Quantifier-Free Separation Logic

lmcs:6548 - Logical Methods in Computer Science, August 10, 2021, Volume 17, Issue 3 - https://doi.org/10.46298/lmcs-17(3:17)2021
A Complete Axiomatisation for Quantifier-Free Separation Logic

Authors: Stéphane Demri ; Étienne Lozes ; Alessio Mansutti

    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.


    Volume: Volume 17, Issue 3
    Published on: August 10, 2021
    Accepted on: May 17, 2021
    Submitted on: June 11, 2020
    Keywords: Computer Science - Logic in Computer Science

    Share

    Consultation statistics

    This page has been seen 308 times.
    This article's PDF has been downloaded 134 times.