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 metadatas

https://hal.univ-lorraine.fr/hal-02980943
Contributor : Didier Galmiche <>
Submitted on : Tuesday, October 27, 2020 - 4:42:07 PM
Last modification on : Thursday, October 29, 2020 - 3:30:32 AM

Links full text

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

12