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...
Những tác giả chính: | , , |
---|---|
Định dạng: | Journal article |
Ngôn ngữ: | English |
Được phát hành: |
Oxford University Press
2021
|