A Logic of Separating Modalities - Université de Lorraine
Article Dans Une Revue Theoretical Computer Science Année : 2016

A Logic of Separating Modalities

Résumé

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 et versions

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

Identifiants

Citer

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⟩
55 Consultations
0 Téléchargements

Altmetric

Partager

More