Partial cut elimination for propositional discrete linear time temporal logic
Articles
Jūratė Sakalauskaitė
Institute of Mathematics and Informatics
Published 2010-12-21
https://doi.org/10.15388/LMR.2010.63
PDF

Keywords

sequent calculi
cut rule
temporal logic
past temporal operators
completeness

How to Cite

Sakalauskaitė J. (2010) “Partial cut elimination for propositional discrete linear time temporal logic”, Lietuvos matematikos rinkinys, 51(proc. LMS), pp. 347–351. doi: 10.15388/LMR.2010.63.

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.

PDF
Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

Please read the Copyright Notice in Journal Policy