Cut-free sequent systems for temporal logic (Q941433)

The paper develops finitary cut-free, invariant-free, weakening-free, and contraction-free sequent calculi for the propositional temporal logics LTL and CTL, using the earlier developed idea of focus games [see, e.g., \textit{M. Lange} and \textit{C. Stirling}, J. Log. Comput. 12, No.~4, 623--639 (2002; Zbl 1001.68077)]. In the case of linear time all rules are invertible. The systems are based on annotating fixpoint formulas with a history, an approach which has also been used in game-theoretic characterisations of these logics.