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 weakeningfree 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. Key words: sequent calculus, temporal logic, cut-free

• Type: Journal
• Year: 2008
• Where: JLP
• Authors: Kai Brünnler, Martin Lange
• Keywords: JLP 2008, Linear Time, Sequent Systems, Temporal Logic