Sekvencinis skaičiavimas be pjūvio, invariantinės taisyklės ir ciklų tikrinimo tiesinio laiko teiginių logikai
Straipsnyje pateikta prisotinimu pagrįsta išsprendžiamumo procedūra tiesinio laiko teiginių logikai (TLTL) su operatoriais „sekantis” ir „visada”. Ši prisotinimo procedūra baigia darbą kai gaunamos tam tikro tipo sekvencijos. TLTL savybės leidžia sukonstruoti polinomonio erdvinio sudėtingumo išsprendžiamumo procedūrą, nenaudojant istorijų, ir ciklų tikrinimo.