Partial cut elimination for propositional discrete linear time temporal logic

Abstract

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.

Keywords

• sequent calculi
• cut rule
• temporal logic
• past temporal operators
• completeness