Cut, invariant rule, and loop-check free sequent calculus for PLTL

Romas  Alonderis; Regimantas  Pliuškevičius

doi:10.15388/LMR.2011.ml02

Articles

Romas Alonderis

Vilnius University

Regimantas Pliuškevičius

Vilnius University

Published 2011-12-15

https://doi.org/10.15388/LMR.2011.ml02

PDF

Keywords

decision procedure
sequent calculus
loop-check
temporal logics
termination

How to Cite

Alonderis, R. and Pliuškevičius, R. (2011) “Cut, invariant rule, and loop-check free sequent calculus for PLTL”, Lietuvos matematikos rinkinys, 52(proc. LMS), pp. 231–236. doi:10.15388/LMR.2011.ml02.

Download Citation

Abstract

In this paper, some loop-check free saturation-like decision procedure is proposed for propositional linear temporal logic (PLTL) with temporal operators “next” and “always”. This saturation procedure terminates when special type sequents are obtained. Properties of PLTL allows us to construct backtracking-free decision procedure without histories and loop-check.

PDF

Downloads

Download data is not yet available.

Most read articles by the same author(s)

Romas Alonderis, Haroldas Giedra, A derivation-loop method for temporal logic , Lietuvos matematikos rinkinys: Vol. 60 (2019): 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, Regimantas Pliuškevičius, Sequent systems for PLTL , 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
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, A labeled sequent calculus for propositional linear time 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 , Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus , Lietuvos matematikos rinkinys: Vol. 48 (2008)
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
Romas Alonderis, Brodsky’s coding method for propositional logic , Lietuvos matematikos rinkinys: Vol. 58 (2017): Ser. A

1 2 3 > >>