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...
| Prif Awduron: | , , |
|---|---|
| Fformat: | Journal article |
| Iaith: | English |
| Cyhoeddwyd: |
Oxford University Press
2021
|
| _version_ | 1826307776948731904 |
|---|---|
| author | Demri, S Fervari, R Mansutti, A |
| author_facet | Demri, S Fervari, R Mansutti, A |
| author_sort | Demri, S |
| collection | OXFORD |
| description | 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 separating conjunction, ◊ is the standard modal operator and ⟨≠⟩ is the difference modality. The calculi only use the logical languages at hand (no external features such as labels) and can be divided in two main parts. First, normal forms for formulae are designed and the calculi allow to transform every formula into a formula in normal form. Second, another part of the calculi is dedicated to the axiomatization for formulae in normal form, which may still require non-trivial developments but is more manageable. |
| first_indexed | 2024-03-07T07:08:10Z |
| format | Journal article |
| id | oxford-uuid:af794bfd-2d5d-4ef0-88d5-3bcab7e7e65e |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:08:10Z |
| publishDate | 2021 |
| publisher | Oxford University Press |
| record_format | dspace |
| spelling | oxford-uuid:af794bfd-2d5d-4ef0-88d5-3bcab7e7e65e2022-05-19T11:13:45ZInternal proof calculi for modal logics with separating conjunctionJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:af794bfd-2d5d-4ef0-88d5-3bcab7e7e65eEnglishSymplectic ElementsOxford University Press2021Demri, SFervari, RMansutti, AModal 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 separating conjunction, ◊ is the standard modal operator and ⟨≠⟩ is the difference modality. The calculi only use the logical languages at hand (no external features such as labels) and can be divided in two main parts. First, normal forms for formulae are designed and the calculi allow to transform every formula into a formula in normal form. Second, another part of the calculi is dedicated to the axiomatization for formulae in normal form, which may still require non-trivial developments but is more manageable. |
| spellingShingle | Demri, S Fervari, R Mansutti, A Internal proof calculi for modal logics with separating conjunction |
| title | Internal proof calculi for modal logics with separating conjunction |
| title_full | Internal proof calculi for modal logics with separating conjunction |
| title_fullStr | Internal proof calculi for modal logics with separating conjunction |
| title_full_unstemmed | Internal proof calculi for modal logics with separating conjunction |
| title_short | Internal proof calculi for modal logics with separating conjunction |
| title_sort | internal proof calculi for modal logics with separating conjunction |
| work_keys_str_mv | AT demris internalproofcalculiformodallogicswithseparatingconjunction AT fervarir internalproofcalculiformodallogicswithseparatingconjunction AT mansuttia internalproofcalculiformodallogicswithseparatingconjunction |