| Title |
Loop-check free sequent calculi for unary fragment of temporal logic |
| Translation of Title |
Becikliai sekvenciniai skaičiavimai unariniam laiko logikos fragmentui. |
| Authors |
Maksimiak, Lukas ; Birštunas, Adomas |
| DOI |
10.15388/LMR.2025.44491 |
| Full Text |
|
| Is Part of |
Lietuvos matematikos rinkinys. Proc. of the Lithuanian Mathematical Society, Ser. A.. Vilnius : Vilniaus universiteto leidykla. 2025, vol. 66, p. 1-10.. ISSN 0132-2818. eISSN 2335-898X |
| Keywords [eng] |
loops ; sequent calculi ; fragments ; PLTL |
| Abstract [eng] |
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 – F1 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 – F3. Elimination of loops was achieved by proving restrictions on the applications of the (⊦ ☐) and (∘) rules. |
| Published |
Vilnius : Vilniaus universiteto leidykla |
| Type |
Journal article |
| Language |
English |
| Publication date |
2025 |
| CC license |
|
