A logic of separating modalities

作者：Courtault Jean Rene; Galmiche Didier; Pym David^*

来源：Theoretical Computer Science, 2016, 637: 30-58.

DOI：10.1016/j.tcs.2016.04.040

• Bunched logic
• Separation logic
• Modal logic
• Resource semantics
• Tableaux
• Concurrency

We present a logic of separating modalities, LSM, that is based on Boolean BI. LSM's modalities, which generalize those of S4, combine, within a quite general relational semantics, BI's resource semantics with modal accessibility. We provide a range of examples illustrating their use for modelling. We give a proof system based on a labelled tableaux calculus with countermodel extraction, establishing its soundness and completeness with respect to the semantics.

• 出版日期2016-7-18