Cut-free sequent systems for temporal logic

10 years 4 months ago
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
Kai Brünnler, Martin Lange
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JLP
Authors Kai Brünnler, Martin Lange
Comments (0)