A Complete Axiomatisation for Quantifier-Free Separation Logic

TL;DR

This paper introduces the first complete internal Hilbert-style axiomatisation for quantifier-free separation logic, grounded in concrete heaplet semantics and without external features, enabling rigorous formal reasoning.

Contribution

It provides the first complete internal axiomatisation for quantifier-free separation logic, integrating concrete semantics and a structured proof system.

Findings

First complete axiomatisation for quantifier-free separation logic

Internal Hilbert-style calculus based on concrete semantics

Structured proof system with elimination of separating connectives

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.