DOAJ Open Access 2024

Grouping based calculus for propositional linear temporal logic

Kostas Ragauskas Adomas Birštunas

Abstrak

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.

Topik & Kata Kunci

Mathematics

Penulis (2)

Kostas Ragauskas

Adomas Birštunas

Format Sitasi

APA MLA BibTeX

Ragauskas, K., Birštunas, A. (2024). Grouping based calculus for propositional linear temporal logic. https://doi.org/10.15388/LMD.2024.37368

Akses Cepat

PDF tidak tersedia langsung

Cek di sumber asli →

Lihat di Sumber doi.org/10.15388/LMD.2024.37368

Informasi Jurnal

Tahun Terbit: 2024
Sumber Database: DOAJ
DOI: 10.15388/LMD.2024.37368
Akses: Open Access ✓