Grouping based calculus for propositional linear temporal logic
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 crea...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Vilnius University Press
2024-12-01
|
| Series: | Lietuvos Matematikos Rinkinys |
| Subjects: | |
| Online Access: | https://ojs.test/index.php/LMR/article/view/37368 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841561084807348224 |
|---|---|
| author | Kostas Ragauskas Adomas Birštunas |
| author_facet | Kostas Ragauskas Adomas Birštunas |
| author_sort | Kostas Ragauskas |
| collection | DOAJ |
| description |
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.
|
| format | Article |
| id | doaj-art-015c1de0032b4d5ba5aea278ca097d2a |
| institution | Kabale University |
| issn | 0132-2818 2335-898X |
| language | English |
| publishDate | 2024-12-01 |
| publisher | Vilnius University Press |
| record_format | Article |
| series | Lietuvos Matematikos Rinkinys |
| spelling | doaj-art-015c1de0032b4d5ba5aea278ca097d2a2025-01-03T06:33:48ZengVilnius University PressLietuvos Matematikos Rinkinys0132-28182335-898X2024-12-0165A10.15388/LMD.2024.37368Grouping based calculus for propositional linear temporal logicKostas Ragauskas0https://orcid.org/0009-0004-3868-6279Adomas Birštunas1https://orcid.org/0000-0003-4574-1534Vilnius UniversityVilnius University 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. https://ojs.test/index.php/LMR/article/view/37368loop checkingsequent calculimarked sequents |
| spellingShingle | Kostas Ragauskas Adomas Birštunas Grouping based calculus for propositional linear temporal logic Lietuvos Matematikos Rinkinys loop checking sequent calculi marked sequents |
| title | Grouping based calculus for propositional linear temporal logic |
| title_full | Grouping based calculus for propositional linear temporal logic |
| title_fullStr | Grouping based calculus for propositional linear temporal logic |
| title_full_unstemmed | Grouping based calculus for propositional linear temporal logic |
| title_short | Grouping based calculus for propositional linear temporal logic |
| title_sort | grouping based calculus for propositional linear temporal logic |
| topic | loop checking sequent calculi marked sequents |
| url | https://ojs.test/index.php/LMR/article/view/37368 |
| work_keys_str_mv | AT kostasragauskas groupingbasedcalculusforpropositionallineartemporallogic AT adomasbirstunas groupingbasedcalculusforpropositionallineartemporallogic |