Nested Sequents for Quantified Modal Logics
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
This paper studies nested sequents for quantified modal logics. In particular, it considers extensions of the propositional modal logics definable by the axioms D, T, B, 4, and 5 with varying, increasing, decreasing, and constant domains. Each calculus is proved to have good structural properties: weakening and contraction are height-preserving admissible and cut is (syntactically) admissible. Each calculus is shown to be equivalent to the corresponding axiomatic system and, thus, to be sound and complete. Finally, it is argued that the calculi are internal -- i.e., each sequent has a formula interpretation -- whenever the existence predicate is expressible in the language.
Details
| Original language | English |
|---|---|
| Title of host publication | Automated Reasoning with Analytic Tableaux and Related Methods |
| Editors | Revantha Ramanayake, Josef Urban |
| Publisher | Springer, Cham |
| Pages | 449–467 |
| Number of pages | 19 |
| ISBN (electronic) | 978-3-031-43513-3 |
| ISBN (print) | 978-3-031-43512-6 |
| Publication status | Published - 2023 |
| Peer-reviewed | Yes |
Publication series
| Series | Lecture Notes in Computer Science |
|---|---|
| Volume | 14278 |
| ISSN | 0302-9743 |
External IDs
| Scopus | 85172418810 |
|---|
Keywords
ASJC Scopus subject areas
Keywords
- Cut elimination, Nested sequent, Quantified modal logic