More efficient proof-search for sequents of temporal logic
The present paper deals with efficiency improvement of backward proof-search of sequents of propositional linear temporal logic, using a loop-type sequent calculus. The improvement is achieved by syntactic transformation of sequents into equivalent to them simpler ones. It is proved that some formu...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Vilnius University Press
2022-12-01
|
| Series: | Lietuvos Matematikos Rinkinys |
| Subjects: | |
| Online Access: | https://www.zurnalai.vu.lt/LMR/article/view/29752 |
| _version_ | 1811188904783511552 |
|---|---|
| author | Romas Alonderis |
| author_facet | Romas Alonderis |
| author_sort | Romas Alonderis |
| collection | DOAJ |
| description |
The present paper deals with efficiency improvement of backward proof-search of sequents of propositional linear temporal logic, using a loop-type sequent calculus. The improvement is achieved by syntactic transformation of sequents into equivalent to them simpler ones. It is proved that some formulas can be removed from sequents with no impact on their derivability.
|
| first_indexed | 2024-04-11T14:26:04Z |
| format | Article |
| id | doaj.art-eefb00cc933d43ef83d7d32d17663c7b |
| institution | Directory Open Access Journal |
| issn | 0132-2818 2335-898X |
| language | English |
| last_indexed | 2024-04-11T14:26:04Z |
| publishDate | 2022-12-01 |
| publisher | Vilnius University Press |
| record_format | Article |
| series | Lietuvos Matematikos Rinkinys |
| spelling | doaj.art-eefb00cc933d43ef83d7d32d17663c7b2022-12-22T04:18:52ZengVilnius University PressLietuvos Matematikos Rinkinys0132-28182335-898X2022-12-0163A10.15388/LMR.2022.29752More efficient proof-search for sequents of temporal logicRomas Alonderis0Vilnius University The present paper deals with efficiency improvement of backward proof-search of sequents of propositional linear temporal logic, using a loop-type sequent calculus. The improvement is achieved by syntactic transformation of sequents into equivalent to them simpler ones. It is proved that some formulas can be removed from sequents with no impact on their derivability. https://www.zurnalai.vu.lt/LMR/article/view/29752temporal logicsbackward proof-searchloop-type sequent calculi |
| spellingShingle | Romas Alonderis More efficient proof-search for sequents of temporal logic Lietuvos Matematikos Rinkinys temporal logics backward proof-search loop-type sequent calculi |
| title | More efficient proof-search for sequents of temporal logic |
| title_full | More efficient proof-search for sequents of temporal logic |
| title_fullStr | More efficient proof-search for sequents of temporal logic |
| title_full_unstemmed | More efficient proof-search for sequents of temporal logic |
| title_short | More efficient proof-search for sequents of temporal logic |
| title_sort | more efficient proof search for sequents of temporal logic |
| topic | temporal logics backward proof-search loop-type sequent calculi |
| url | https://www.zurnalai.vu.lt/LMR/article/view/29752 |
| work_keys_str_mv | AT romasalonderis moreefficientproofsearchforsequentsoftemporallogic |