Nested Sequents for Quantified Modal Logics

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Beitragende

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

OriginalspracheEnglisch
TitelAutomated Reasoning with Analytic Tableaux and Related Methods
Redakteure/-innenRevantha Ramanayake, Josef Urban
Herausgeber (Verlag)Springer, Cham
Seiten449–467
Seitenumfang19
ISBN (elektronisch)978-3-031-43513-3
ISBN (Print)978-3-031-43512-6
PublikationsstatusVeröffentlicht - 2023
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science
Band14278
ISSN0302-9743

Externe IDs

Scopus 85172418810

Schlagworte

Schlagwörter

  • Cut elimination, Nested sequent, Quantified modal logic