Straipsnyje pateiktas korektiškas ir pilnas sekvencinis skaičiavimas tiesinei laiko logikai. Įrodymų baigtinumo nustatymui pateiktas naujas metodas naudojantis žymes. Šis metodas leidžia efektyviai taikyti modalines taisykles nagrinėjamai laiko logikai.