Open AccessCut, invariant rule, and loop-check free sequent calculus for PLTL
Author(s) -
Romas Alonderis,
Regimantas Pliuškevičius
Publication year - 2011
Publication title -
lietuvos matematikos rinkinys
Language(s) - English
Resource type - Journals
eISSN - 2335-898X
pISSN - 0132-2818
DOI - 10.15388/lmr.2011.ml02
Subject(s) - sequent , sequent calculus , mathematics , natural deduction , invariant (physics) , propositional calculus , calculus (dental) , algorithm , computer science , discrete mathematics , medicine , geometry , dentistry , mathematical proof , mathematical physics
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.