A derivation-loop method for temporal logic
Articles
Romas Alonderis
Vilnius University
https://orcid.org/0000-0002-7792-5285
Haroldas Giedra
Vilnius University
https://orcid.org/0000-0002-6852-5909
Published 2019-11-12
https://doi.org/10.15388/LMR.A.2019.14953
PDF

Keywords

temporal logics
sequent calculi
derivation loops

How to Cite

Alonderis R. and Giedra H. (2019) “A derivation-loop method for temporal logic”, Lietuvos matematikos rinkinys, 60(A), pp. 1-6. doi: 10.15388/LMR.A.2019.14953.

Abstract

Various types of calculi (Hilbert, Gentzen sequent, resolution calculi, tableaux) for propositional linear temporal logic (PLTL) have been considered in the literature. Cutfree Gentzen-type sequent calculi are convenient tools for backward proof-search search of formulas and sequents. In this paper we present a cut-free Gentzen type sequent calculus for PLTL with the operator

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