Open AccessA labeled sequent calculus for propositional linear time logic
Author(s) -
Romas Alonderis
Publication year - 2012
Publication title -
lietuvos matematikos rinkinys
Language(s) - English
Resource type - Journals
eISSN - 2335-898X
pISSN - 0132-2818
DOI - 10.15388/lmr.a.2012.01
Subject(s) - sequent , sequent calculus , propositional calculus , natural deduction , cut elimination theorem , proof calculus , calculus (dental) , mathematics , propositional variable , zeroth order logic , discrete mathematics , computer science , intermediate logic , theoretical computer science , medicine , geometry , dentistry , mathematical proof , description logic , multimodal logic
A labeled sequent calculus LSC for propositional linear discrete time logic PLTL is introduced. Its sub-calculus LSC−TL is proved to be complete for some class of PLTL sequents.