Skip to Main content Skip to Navigation
Journal articles

A Logic of Separating Modalities

Abstract : 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.
Document type :
Journal articles
Complete list of metadata
Contributor : Didier Galmiche Connect in order to contact the contributor
Submitted on : Tuesday, October 27, 2020 - 4:42:07 PM
Last modification on : Wednesday, November 3, 2021 - 7:57:42 AM

Links full text




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



Record views