Ciklų aptikimas sekvenciniuose skaičiavimuose

Ištrauka

Ciklų aptikimas sekvenciniuose skaičiavimuose
Baigiamasis bakalauro darbas

Turinys
ĮVADAS 3
1. SEKVENCINIAI SKAIČIAVIMAI 4
1.1 SĄVOKOS BEI APIBRĖŽIMAI 4
2. TIESINĖ LAIKO LOGIKA PLTL – SKAIČIAVIMAS GLPLTL 7
2.1 SINTAKSĖ IR SEMANTIKA 7
2.2 CIKLO STRUKTŪRA IR ATSIRADIMO PRIEŽASTYS 7
2.3 CIKLO APTIKIMO BŪDAS – ŽYMIŲ METODAS 10
3. TIESINĖS LAIKO LOGIKOS PLTL CIKLŲ APTIKIMO PATOBULINIMAS 13
3.1 TAISYKLIŲ TAIKYMO TVARKA 13
3.2 SAVYBĖS VIENETINIO TEIGIAMO CIKLO ILGIO NUSTATYMUI HIPOTEZĖ 14
3.3 CIKLO NEGALIMUMO SAVYBĖS 14
3.4 SEKVENCIJŲ GRUPAVIMAS 19
3.5 CIKLO NEGALIMUMO APTIKIMO METODAS 20
3.6 CIKLŲ TIPO NUSTATYMO METODAS 20
3.7 SKAIČIAVIMAS G*TL 22
3.8 (GROUP) TAISYKLĖS SUDĖTINGUMO ĮVERTINIMAS 23
3.9 CIKLŲ APTIKIMO SKAIČIAVIME G*TL SUDĖTINGUMO ĮVERTINIMAS 24
IŠVADOS IR REZULTATAI 27
ŠALTINIAI 28

Įvadas
Sekvenciniai skaičiavimai yra galingas įrankis, naudojamas automatizuotam loginių formulių
išvedimui. Paprasčiausi sekvenciniai skaičiavimai yra skirti tradicinei (teiginių) matematinei
logikai – tokie skaičiavimai vadinami Gentzeno (dar žymimi raide G) ir buvo sukurti dar 1934
metais. Žinoma, šiais laikais yra labiau aktualu analizuoti sekvencinius skaičiavimus ir kitokioms
logikoms – modalumo, laiko, intuicionistinei ir t.t. Šių logikų sekvenciniai skaičiavimai gali būti
naudingi ir inovatyviose srityse, pavyzdžiui, dirbtinio intelekto sprendimuose.
Sekvencinius skaičiavimus įvairioms logikoms vienija taisyklės, kurių pagalba iš pradinės
sekvencijos yra konstruojamas jos išvedimo medis. Jei išvedimo metu nepavyksta gauti tinkamo
išvedimo medžio, tai dar nereiškia, jog sekvencija yra neišvedama – gali būti, kad tiesiog
nepavyko parinkti tokios (palankios) taisyklių taikymo sekos tinkamam išvedimui. Tačiau ši
problema yra neesminė, kadangi grubios jėgos (angl. brute force) pagalba galingi kompiuteriai
jau geba perbėgti visus įmanomus medžio konstravimo variantus ir rasti, ar sekvencija yra
išvedama, jei skaičiavimas nėra begalinis.
Žymiai didesnė problema – ciklai. Gali būti, jog išvedimo medžio konstravimo metu
panaudoję tam tikrą taisyklių seką grįšime prie sekvencijos, kurią jau buvome gavę anksčiau,
taip patekdami į savotišką ciklą. Grubi jėga šioje vietoje nėra efektyvus sprendimas, kadangi
atsiradus begaliniams ciklams visų variantų perranka tampa praktiškai neįmanoma. Ši problema
yra aktuali ir šiandien, o literatūroje galima rasti nemažai aprašytų būdų ciklams aptikti ar net
eliminuoti (pavyzdžiui, įvairūs ciklų tipai bei aptikimo būdai yra nagrinėjami darbuose [HSZ95],
[KSD09] bei [SD10]). Atsižvelgiant į problemą bei jos aktualumą galime suformuluoti darbo tikslą.
Darbo tikslas – Sukurti sekvencinio skaičiavimo tiesinei laiko logikai patobulinimą, kuris
leistų efektyviau aptikti ciklus.
Uždaviniai:
Nustatyti ciklų susidarymo būtinasias sąlygas.
Rasti ciklo paieškos bei jo tipo nustatymo patobulinimų.
Įkomponuoti patobulinimus į skaičiavimo taisykles, taip sukuriant naują skaičiavimą.
Įvertinti optimizuoto ciklų aptikimo metodo sudėtingumą bei pagerinimus.