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 $\omega$-type rule.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Please read the Copyright Notice in Journal Policy.