Šiame straipsnyje pateikiamas dalinis metodas leidžiantis gauti efektyvesnę sekvencijų įrodymo paiešką propozicinei tiesinio laiko logikai, naudojant ciklinį sekvencinį skaičiavimą. Šis metodas yra pagrįstas sintaksine sekvencijų transformacija į joms ekvivalenčias paprastesnes sekvencijas. Straipsnyje taip pat parodoma, kad kai kurios formulės gali būti pašalintos iš sekvencijų niekaip nepaveikiant jų įrodomumo.