@inproceedings{5de553abc6884e86b664a54f0dc7ce7b,
title = "Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents",
abstract = "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.",
author = "Rajeev Gor{\'e} and Bj{\"o}rn Lellmann",
note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.; 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019 ; Conference date: 03-09-2019 Through 05-09-2019",
year = "2019",
doi = "10.1007/978-3-030-29026-9\_11",
language = "English",
isbn = "9783030290252",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "185--202",
editor = "Serenella Cerrito and Andrei Popescu",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings",
address = "Germany",
}