Sequent systems for PLTL
Articles
Romas Alonderis
Vilnius University
Regimantas Pliuškevičius
Vilnius University
Published 2013-12-15
https://doi.org/10.15388/LMR.A.2013.03
PDF

Keywords

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.

Abstract

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.

PDF
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 > >>