Mechanised uniform interpolation for modal logics K, GL, and iSL
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914774749544448 |
|---|---|
| author | Férée, Hugo van der Giessen, Iris van Gool, Sam Shillito, Ian |
| author_facet | Férée, Hugo van der Giessen, Iris van Gool, Sam Shillito, Ian |
| contents | The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) Gödel-Löb logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong Löb logic iSL, for which this is the first proof-theoretic construction of uniform interpolants. Our work also yields verified programs that allow one to compute the propositional quantifiers on any formula in this logic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_10494 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Mechanised uniform interpolation for modal logics K, GL, and iSL Férée, Hugo van der Giessen, Iris van Gool, Sam Shillito, Ian Logic in Computer Science Logic 03B45, 03B20, 03F45, 68V20 F.4.1; I.2.3; I.2.4 The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) Gödel-Löb logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong Löb logic iSL, for which this is the first proof-theoretic construction of uniform interpolants. Our work also yields verified programs that allow one to compute the propositional quantifiers on any formula in this logic. |
| title | Mechanised uniform interpolation for modal logics K, GL, and iSL |
| topic | Logic in Computer Science Logic 03B45, 03B20, 03F45, 68V20 F.4.1; I.2.3; I.2.4 |
| url | https://arxiv.org/abs/2402.10494 |