A derivation-loop method for temporal logic - Alonderis, Romas; Giedra, Haroldas (Lietuvos matematikos rinkinys, 2019)
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
Keywords: temporal logics; sequent calculi; derivation loops