TY - GEN
T1 - Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents
AU - Goré, Rajeev
AU - Lellmann, Björn
N1 - Publisher Copyright:
© 2019, Springer Nature Switzerland AG.
PY - 2019
Y1 - 2019
N2 - We give a linear nested sequent calculus for the basic normal tense logic Kt. 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.
AB - We give a linear nested sequent calculus for the basic normal tense logic Kt. 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.
UR - http://www.scopus.com/inward/record.url?scp=85077118412&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-29026-9_11
DO - 10.1007/978-3-030-29026-9_11
M3 - Conference contribution
SN - 9783030290252
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 185
EP - 202
BT - Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings
A2 - Cerrito, Serenella
A2 - Popescu, Andrei
PB - Springer
T2 - 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019
Y2 - 3 September 2019 through 5 September 2019
ER -