Open AccessRestrictions for loop-check in sequent calculus for temporal logic
Author(s) -
Adomas Birštunas
Publication year - 2008
Publication title -
lietuvos matematikos rinkinys
Language(s) - English
Resource type - Journals
eISSN - 2335-898X
pISSN - 0132-2818
DOI - 10.15388/lmr.2008.18108
Subject(s) - sequent , cut elimination theorem , sequent calculus , natural deduction , proof calculus , calculus (dental) , mathematics , computer science , algorithm , discrete mathematics , mathematical proof , medicine , geometry , dentistry
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.