Internal proof calculi for modal logics with separating conjunction
Modal separation logics are formalisms that combine modal operators to reason locally, with separating connectives that allow to perform global updates on the models. In this work, we design Hilbert-style proof systems for the modal separation logics MSL(∗,⟨≠⟩) and MSL(∗,◊), where ∗ is the separati...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Oxford University Press
2021
|