论文标题
无量词分离逻辑的完整的公理化
A Complete Axiomatisation for Quantifier-Free Separation Logic
论文作者
论文摘要
我们提出了第一个完整的公理化，用于无量词的分离逻辑。该逻辑配备了标准的混凝土堆语义，并且证明系统没有外部功能，例如名义/标签。由于需要考虑具体语义，因此不可能完全依靠布尔BI的证明系统。因此，我们提出了第一个用于无量词分离逻辑的Hilbert式公理化。微积分分为三个部分：核心公式的公理化，其中核心公式的布尔组合捕获了整个逻辑，公理和推理规则的表达，以模拟分离连接的自下而上消除，最后是结构公理和结构性公理和推理规则，并从命题的计算和bior bi a image bi with ogage with ogage with。
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.
