Cut, invariant rule, and loop-check free sequent calculus for PLTL
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.

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
Creative Commons License

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

Please read the Copyright Notice in Journal Policy