| Title |
Restrictions for loop-check in sequent calculus for temporal logic / |
| Translation of Title |
Apribojimai ciklų radimui sekvenciniame laiko logikos skaičiavime. |
| Authors |
Birštunas, Adomas |
| DOI |
10.15388/LMR.2008.18108 |
| Full Text |
|
| Is Part of |
Lietuvos matematikos rinkinys.. Vilnius : Vilniaus universiteto leidykla. 2008, t. 48-49, p. 269-274.. ISSN 0132-2818. eISSN 2335-898X |
| Keywords [eng] |
sequent calculus ; temporal logic ; efficient loop-check |
| Abstract [eng] |
In this paper, we present sequent calculus for linear temporal logic. This sequent calculus uses efficient loop-check technique. We prove that we can use not all but only several special sequents from the derivation tree for the loop-check. We use indexes to discover these special sequents in the sequent calculus. These restrictions let us to get efficient decision procedure based on introduced sequent calculus. |
| Published |
Vilnius : Vilniaus universiteto leidykla |
| Type |
Journal article |
| Language |
English |
| Publication date |
2008 |
| CC license |
|
