| Title |
A derivation-loop method for temporal logic |
| Translation of Title |
Įrodymo ciklų metodas laiko logikai. |
| Authors |
Alonderis, Romas ; Giedra, Haroldas |
| DOI |
10.15388/LMR.A.2019.14953 |
| Full Text |
|
| Is Part of |
Lietuvos matematikos rinkinys. Ser. A.. Vilnius : Vilniaus universiteto leidykla. 2019, t. 60, p. 1-6.. ISSN 0132-2818. eISSN 2335-898X |
| Keywords [eng] |
temporal logics ; sequent calculi ; derivation loops. |
| Abstract [eng] |
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 “until”. We show that the calculus is sound and complete for the considered logic. |
| Published |
Vilnius : Vilniaus universiteto leidykla |
| Type |
Journal article |
| Language |
English |
| Publication date |
2019 |
