Restrictions for loop-check in sequent calculus for temporal logic

Autor:	Adomas Birštunas
Jazyk:	English<br />Lithuanian
Rok vydání:	2008
Předmět:	sequent calculus temporal logic efficient loop-check Mathematics QA1-939
Zdroj:	Lietuvos Matematikos Rinkinys, Vol 48, Iss proc. LMS (2008)
Druh dokumentu:	article
ISSN:	0132-2818 2335-898X 75296284
DOI:	10.15388/LMR.2008.18108
Popis:	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.
Databáze:	Directory of Open Access Journals
Externí odkaz:	https://doaj.org/article/bd6ab75296284f42bdfa8d14b76832a1 Zobrazit plný text záznamu View record in DOAJ