  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.

Logic in Computer Science