Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6875913 | Theoretical Computer Science | 2016 | 29 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Jean-René Courtault, Didier Galmiche, David Pym,