Restrictions for loop-check in sequent calculus for temporal logic

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 se...

Full description

Bibliographic Details
Main Author: Adomas Birštunas
Format: Article
Language:English
Published: Vilnius University Press 2008-12-01
Series:Lietuvos Matematikos Rinkinys
Subjects:
Online Access:https://www.journals.vu.lt/LMR/article/view/18108