| Title |
Sequent systems for PLTL / |
| Another Title |
Sekvencinės sistemos PTL logikai. |
| Authors |
Alonderis, Romas ; Pliuškevičius, Regimantas Ričardas |
| DOI |
10.15388/LMR.A.2013.03 |
| Full Text |
|
| Is Part of |
Lietuvos matematikos rinkinys. Ser. A.. Vilnius : Vilniaus universiteto leidykla. 2013, t. 54, p. 1-5.. ISSN 0132-2818. eISSN 2335-898X |
| Keywords [eng] |
temporal logics ; sequent calculi ; ω-type rule ; weak-induction rule ; lLooping axioms ; invariant-like rule |
| Abstract [eng] |
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. |
| Published |
Vilnius : Vilniaus universiteto leidykla |
| Type |
Journal article |
| Language |
English |
| Publication date |
2013 |
| CC license |
|
