Sequent systems for PLTL - Alonderis, Romas; Pliuškevičius, Regimantas (Lietuvos matematikos rinkinys, 2013)
We consider three sequent calculi for propositional linear temporal logic (PLTL) which allow us to formalize the properties of operator “always”. The main new results presented in the paper are: (1) introduction of the calculus with looping axioms; (2) the direct proof that the presented calculi are equivalent; (3) the proof of completeness of the calculi with looping axioms and with invariant-like rule based on completeness of the calculus with the infinitary ω-type rule.