Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents
Loading...
Date
Authors
Gore, Rajeev
Lellmann, Bjorn
Journal Title
Journal ISSN
Volume Title
Publisher
Springer, Cham
Abstract
We give a linear nested sequent calculus for the basic normal tense logic 𝖪𝗍 We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut-elimination. Linear nested sequents thus provide the minimal amount of nesting necessary to provide an adequate proof-theory for modal logics containing converse. As a bonus, this yields a cut-free calculus for symmetric modal logic KB.
Description
Keywords
Citation
Goré, R., Lellmann, B. (2019). Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents. In: Cerrito, S., Popescu, A. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2019. Lecture Notes in Computer Science(), vol 11714. Springer, Cham. https://doi.org/10.1007/978-3-030-29026-9_11
Collections
Source
Automated Reasoning with Analytic Tableaux and Related Methods
Type
Book Title
Entity type
Access Statement
License Rights
Restricted until
2099-12-31
Downloads
File
Description