Šiame darbe nagrinėjamas efektyvaus sekvencinio skaičiavimo konstravimas pasirinktam tiesinės teiginių laiko logikos (PLTL) fragmentui, praplečiant klasikinio skaičiavimo idėjas, aptartas [1], ir remiantis ankstesniais tyrimais apie ciklus PLTL logikoje. Apibrėžtas unarinis tiesinės laiko logikos fragmentas, kuriame formulėse gali būti daugiausiai vienas išorinis ☐ (,,visada``) operatorius. Fragmentai paprastai analizuojami siekiant apibrėžti efektyvesnius skaičiavimus formulėms, priklausančioms fragmentui, ypač kai tai nėra įmanoma visai logikai (tokia strategija naudojama [3,4]). Pristatoma nauja or-tipo sukcedente taiyklė (⊦ ☐L*) Autoriai siūlo naują sekvencinį skaičiavimą PLTL – F1 fragmentui α, kuris pašalina ciklines aksiomas ir pagerina išvedimo efektyvumą. Be to, autoriai pristato ir pilnai beciklį skaičiavimą PLTL – F3. Ciklų pašalinimas buvo pasiektas įrodžius (⊦ ☐) ir (∘) taisyklių taikymo apribojimus.
Šis darbas apsaugotas Creative Commons priskyrimo 4.0 viešąja licencija.