Literatūroje yra nagrinėjamos įvairios propozicinės tiesinės laiko logikos dedukcinės sistemos, tokios kaip: Hilberto tipo skaičiavimai, Gentzeno tipo sekvenciniai skaičiavimai, rezoliucijų ir lentelių metodai. Pjūvio taisyklės neturintys Gentzeno tipo sekvenciniai skaičiavimai leidžia efektyviai atlikti atgalinę formulių ir sekvencijų įrodymo paiešką, siekiant patikrinti jų tapatų teisingumą. Šiame straipsnyje pateikiamas pjūvio taisyklės neturintis Gentzeno tipo sekvencinis skaičiavimas propozicinei tiesinei laiko logikai su operatoriumi “kol”. Parodoma, kad šis skaičiavimas yra korektiškas ir pilnas nagrinėjamos logikos atžvilgiu.