Restrictions for loop-check in sequent calculus for temporal logic with until operator - Birštunas, Adomas (Lietuvos matematikos rinkinys, 2009)
In this paper, we present sequent calculus for branching-time temporal logic with until operator. This sequent calculus uses efficient loop-checktechinque. 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.
Keywords: sequent calculus; branchnig-time temporal logic; until operator; loop-check