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

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

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 backt...

Full description

Bibliographic Details
Main Authors: Romas Alonderis, Regimantas Pliuškevičius
Format: Article
Language:English
Published: Vilnius University Press 2011-12-01
Series:Lietuvos Matematikos Rinkinys
Subjects:
decision procedure
sequent calculus
loop-check
temporal logics
termination
Online Access:https://www.journals.vu.lt/LMR/article/view/15430

Internet

https://www.journals.vu.lt/LMR/article/view/15430

Similar Items