Restrictions for loop-check in sequent calculus for temporal logic

Lietuvos Matematikos Rinkinys

AdomasBirštunas¹ 

[1] Vilnius University;

关键词: sequent calculus;    temporal logic;    efficient loop-check;   

DOI  :  10.15388/LMR.2008.18108

来源: DOAJ

【 摘 要 】

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.

【 授权许可】

Unknown