Sequent systems for PLTL
Romas Alonderis
Vilnius University
Regimantas Pliuškevičius
Vilnius University
Published 2013-12-15


temporal logics
sequent calculi
$\omega$-type rule
weak-induction rule
looping axioms
invariant-like rule

How to Cite

Alonderis R. and Pliuškevičius R. (2013) “Sequent systems for PLTL”, Lietuvos matematikos rinkinys, 54(A), pp. 1–5. doi: 10.15388/LMR.A.2013.03.


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.

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

Please read the Copyright Notice in Journal Policy

Most read articles by the same author(s)

1 2 > >>