Inproceedings3360: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Keine Bearbeitungszusammenfassung |
Keine Bearbeitungszusammenfassung |
||
| Zeile 16: | Zeile 16: | ||
|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. | |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. | ||
|Download=NestedSequentsQML.pdf | |Download=NestedSequentsQML.pdf | ||
|Slides=Talk - Lyon.pdf | |||
|DOI Name=10.1007/978-3-031-43513-3_24 | |DOI Name=10.1007/978-3-031-43513-3_24 | ||
|Projekt=DeciGUT | |Projekt=DeciGUT | ||
|Forschungsgruppe=Computational Logic | |Forschungsgruppe=Computational Logic | ||
}} | }} | ||
Aktuelle Version vom 4. Oktober 2023, 12:22 Uhr
Tim Lyon, Eugenio Orlandelli
Nested Sequents for Quantified Modal Logics
In Revantha Ramanayake, Josef Urban, eds., Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023), 449--467, 2023
Nested Sequents for Quantified Modal Logics
In Revantha Ramanayake, Josef Urban, eds., Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023), 449--467, 2023
- KurzfassungAbstract
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. - Projekt:Project: DeciGUT
- Forschungsgruppe:Research Group: Computational LogicComputational Logic
@inproceedings{LO2023,
author = {Tim Lyon and Eugenio Orlandelli},
title = {Nested Sequents for Quantified Modal Logics},
editor = {Revantha Ramanayake and Josef Urban},
booktitle = {Proceedings of Automated Reasoning with Analytic Tableaux and
Related Methods (TABLEAUX 2023)},
year = {2023},
pages = {449--467},
doi = {10.1007/978-3-031-43513-3_24}
}
