Gore, RajeevLellmann, BjornCerrito, S.Popescu, A .2023-11-29SeptemberGoré, 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_11978-3-030-29026-90302-9743http://hdl.handle.net/1885/307522We 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.application/pdfen-AU© 2019 Springer Nature Switzerland AG2019-08-1410.1007/978-3-030-29026-9_112022-08-28