Loop-check free sequent calculi for unary fragment of temporal logic

Abstract

This paper explores the construction of an efficient sequent calculus for a selected fragment of porpositional linear temporal logic (PLTL), extending the ideas of classical calculi discussed in [1], and builds upon previous investigations into the issue of loops in PLTL. Unary fragment of PLTL is identified in which formulas can contain at most one outermost ☐ (``always'') operator. Fragments are typically analyzed with the aim of defining more efficient calculi for formulas belonging to the fragment, especially when such an approach is not feasible for the full logic (such a strategy is employed in [3,4]). New or-type rule (⊦ ☐_L*) is introduced by  the authors. Authors propose newly developed sequent calculus PLTL – F₁  for this fragment, which eliminates the need for loop axioms while improving derivation efficiency. Furthermore, the authors also introduce a totally loop-check free sequent calculus PLTL – F₃. Elimination of loops was achieved by proving restrictions on the applications of the (⊦ ☐) and (∘) rules.