Open AccessPartial cut elimination for propositional discrete linear time temporal logic
Author(s) -
Jūratė Sakalauskaitė
Publication year - 2010
Publication title -
lietuvos matematikos rinkinys
Language(s) - English
Resource type - Journals
eISSN - 2335-898X
pISSN - 0132-2818
DOI - 10.15388/lmr.2010.63
Subject(s) - sequent , soundness , completeness (order theory) , natural deduction , sequent calculus , mathematics , linear temporal logic , cut elimination theorem , temporal logic , sketch , linear logic , propositional calculus , calculus (dental) , zeroth order logic , discrete mathematics , intuitionistic logic , proof calculus , algorithm , computer science , programming language , multimodal logic , mathematical analysis , description logic , medicine , geometry , dentistry , mathematical proof
We consider propositional discrete linear time temporal logic with future and past operators of time. For each formula ϕ of this logic, we present Gentzen-type sequent calculus Gr(ϕ) with a restricted cut rule. We sketch a proof of the soundness and the completeness of the sequent calculi presented. The completeness is proved via construction of a canonical model.