Dalinis pjūvio pašalinimas teiginių diskretinei laiko logikai

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.Pateikiami Gentzeno tipo sekvenciniai skaičiavimai teiginių tiesinio laiko logikai su ateities ir praeities laiko operatoriais. Šiuose skaičiavimuose pjūvio formulės priklauso baigtinei formulių aibei. Įrodomas šių skaičiavimų korektiškumas ir pilnumas