Sequent systems for PLTL

Romas Alonderis; Regimantas Pliuškevičius

doi:10.15388/LMR.A.2013.03

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

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

Please read the Copyright Notice in Journal Policy.

Downloads

Article Views | PDF Downloads

Range Graph | Chart Graph

Most read articles by the same author(s)

Romas Alonderis, A labeled sequent calculus for propositional linear time logic , Lietuvos matematikos rinkinys: Vol 53 (2012): Ser. A
Aurimas Paulius Girčys, Regimantas Pliuškevičius, Two complete finitary sequent calculi for reflexive common knowledge , Lietuvos matematikos rinkinys: Vol 54 (2013): Ser. A
Regimantas Pliuškevičius, Aurimas Paulius Girčys, Saturation method for reflexive common knowledge logic , Lietuvos matematikos rinkinys: Vol 53 (2012): Ser. A
Regimantas Pliuškevičius, Method of marks for propositional linear temporal logic , Lietuvos matematikos rinkinys: Vol 55 (2014): Ser. A
Romas Alonderis, Regimantas Pliuškevičius, Aida Pliuškevičienė, Finite sequent calculi for PLTL , Lietuvos matematikos rinkinys: Vol 56 (2015): Ser. A
Romas Alonderis, Haroldas Giedra, A derivation-loop method for temporal logic , Lietuvos matematikos rinkinys: Vol 60 (2019): Ser. A
Romas Alonderis, Brodsky’s coding method for propositional logic , Lietuvos matematikos rinkinys: Vol 58 (2017): Ser. A
Haroldas Giedra, Romas Alonderis, Applications of logic of correlated knowledge to quantum mechanics , Lietuvos matematikos rinkinys: Vol 59 (2018): Ser. A
Romas Alonderis, A sequent calculus for propositional temporal logic with time gaps , Lietuvos matematikos rinkinys: Vol 52 (2011)
Romas Alonderis, Regimantas Pliuškevičius, Cut, invariant rule, and loop-check free sequent calculus for PLTL , Lietuvos matematikos rinkinys: Vol 52 (2011)

1 2 > >>