| Title |
More efficient proof-search for sequents of temporal logic |
| Translation of Title |
Efektyvesnė laiko logikos sekvencijų įrodymo paieška. |
| Authors |
Alonderis, Romas |
| DOI |
10.15388/LMR.2022.29752 |
| Full Text |
|
| Is Part of |
Lietuvos matematikos rinkinys. Proc. of the Lithuanian Mathematical Society. Ser. A.. Vilnius : Vilniaus universiteto leidykla. 2022, t. 63, p. 1-8.. ISSN 0132-2818. eISSN 2335-898X |
| Keywords [eng] |
temporal logics ; backward proof-search ; loop-type sequent calculi |
| Abstract [eng] |
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. |
| Published |
Vilnius : Vilniaus universiteto leidykla |
| Type |
Journal article |
| Language |
English |
| Publication date |
2022 |
| CC license |
|