Cut-free sequent systems for temporal logic

Currently known sequent systems for temporal logics such as linear time temporal logic and computation tree logic either rely on a cut rule, an invariant rule, Or an infinitary rule. The first and second violate the subformula property and the third has infinitely many premises. We present finitary cut-free invariant-free weakening-free and contraction-free sequent systems for both logics mentioned. 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. (C) 2008 Elsevier Inc. All rights reserved.