| Title |
Restrictions for loop-check in sequent calculus for temporal logic with until operator |
| Translation of Title |
Apribojimai ciklų radimui sekvenciniame laiko logikos skaičiavime su until operatoriumi. |
| Authors |
Birštunas, Adomas |
| DOI |
10.15388/LMR.2009.44 |
| Full Text |
|
| Is Part of |
Lietuvos matematikos rinkinys.. Vilnius : Vilniaus universiteto leidykla. 2009, t. 50, p. 247-252.. ISSN 0132-2818. eISSN 2335-898X |
| Keywords [eng] |
sequent calculus ; branchnig-time temporal logic ; until operator ; loop-check |
| Abstract [eng] |
In this paper, we present sequent calculus for branching-time temporal logic with until operator. This sequent calculus uses efficient loop-check techinque. 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 |
2009 |
| CC license |
|
