一句话：提出无量词分离逻辑的首个内蕴希尔伯特式完全公理化。
本文研究无量词分离逻辑的完全公理化问题。该逻辑采用标准的具体 heaplet 语义，且证明系统不引入 nominals/labels 等外部机制；作者指出不能完全依赖 Boolean BI 的证明系统，因为必须纳入具体语义。为此，他们给出首个内蕴希尔伯特式公理化，分为三部分：核心公式的公理，其布尔组合足以表达整个逻辑；模拟自底向上消除分离连接词的公理与推理规则；以及来自命题演算和带 magic wand 的 Boolean BI 的结构公理与推理规则。该工作建立了该逻辑的完整公理化。
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.
@article{paperbot1288,
title = {A Complete Axiomatisation for Quantifier-Free Separation Logic},
author = {Stéphane Demri and Étienne Lozes and Alessio Mansutti},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:17)2021}
}