Partial cut elimination for propositional discrete linear time temporal logic - Sakalauskaitė, Jūratė (Lietuvos matematikos rinkinys, 2010)
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.