Restrictions for loop-check in sequent calculus for temporal logic
Adomas Birštunas
Vilnius University
Published 2008-12-21


sequent calculus
temporal logic
efficient loop-check

How to Cite

Birštunas A. (2008) “Restrictions for loop-check in sequent calculus for temporal logic”, Lietuvos matematikos rinkinys, 48(proc. LMS), pp. 269–274. doi: 10.15388/LMR.2008.18108.


In this paper, we present sequent calculus for linear temporal logic. 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.

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

Please read the Copyright Notice in Journal Policy