Title |
Partial cut elimination for propositional discrete linear time temporal logic |
Another Title |
Dalinis pjūvio pašalinimas teiginių diskretinei laiko logikai. |
Authors |
Sakalauskaitė, Jūratė |
DOI |
10.15388/LMR.2010.63 |
Full Text |
|
Is Part of |
Lietuvos matematikos rinkinys. Lietuvos matematikų draugijos darbai. 2010, T. 51, p. 347-351.. ISSN 0132-2818 |
Keywords [eng] |
Calculus, sequent ; Cut rule ; Logic, temporal ; Past temporal operators ; Completeness |
Abstract [eng] |
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 G_r(φ) 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. |
Type |
Conference paper |
Language |
English |
Publication date |
2010 |
CC license |
|