| Title |
Grouping based calculus for propositional linear temporal logic / |
| Translation of Title |
Grupavimu paremtas tiesinės teiginių laiko logikos skaičiavimas. |
| Authors |
Ragauskas, Kostas ; Birštunas, Adomas |
| DOI |
10.15388/LMD.2024.37368 |
| Full Text |
|
| Is Part of |
Lietuvos matematikos rinkinys. Ser. A.. Vilnius : Vilniaus universiteto leidykla. 2024, t. 65, p. 18-24.. ISSN 0132-2818. eISSN 2335-898X |
| Keywords [eng] |
loop checking ; sequent calculi ; marked sequents |
| Abstract [eng] |
In this paper, the authors research the problem of loops in linear temporal logic PLTL. The task involves defining the standard rule application process for the derivation procedure (as used in [4] and [5]), determining and proving properties for the absence of a loop beneath some sequent, and creating a new calculus G*TL, which uses the proposed sequent grouping method, along with the method of marks (similar marking concepts were proposed in [5] and [6]). A new type of structural rule (GROUP), along with a modification of the rule (∘) to (∘*) is introduced. Finally, it is shown that the loop checking mechanism used in calculus G*TL is efficient, comparing it with other known calculi for logic PLTL. |
| Published |
Vilnius : Vilniaus universiteto leidykla |
| Type |
Journal article |
| Language |
English |
| Publication date |
2024 |
| CC license |
|
