A Logic of Separating Modalities - Université de Lorraine Access content directly
Journal Articles Theoretical Computer Science Year : 2016

A Logic of Separating Modalities


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.

Dates and versions

hal-02980943 , version 1 (27-10-2020)



Jean-René Courtault, Didier Galmiche, David Pym. A Logic of Separating Modalities. Theoretical Computer Science, 2016, 637 (1), pp.30-58. ⟨10.1016/j.tcs.2016.04.040⟩. ⟨hal-02980943⟩
37 View
0 Download



Gmail Facebook X LinkedIn More