ZÁVEREČNÁ PRÁCA

Meno a priezvisko študenta: Norbert Jurík
Študijný program: aplikovaná informatika (Jednoodborové štúdium, bakalársky I. st., denná forma)
Študijný obor: aplikovaná informatika
Typ záverečnej práce: bakalárska
Jazyk záverečnej práce: slovenský
Sekundárny jazyk: anglický

Názov:
Webový editor rezolvenčných dôkazov
Web-Based Editor of Resolution Proofs

Anotácia:
V rámci predmetu Matematika (4) – Logika pre informatikov vyučujeme okrem iných aj rezolvenčný kalkul pre logiku prvého rádu a s ním súvisiace úpravy formúl do klauzálnej formy a skolemizáciu. Existujúce nástroje na kontrolu a poskytovanie spätnej väzby k formálnym dôkazom, či už vytvorené pre náš ale aj iné podobné kurzy, buď nepodporujú tento formálny systém alebo automatizujú niektoré jeho časti, čo zabraňuje študentom v získaní konkrétnej skúsenosti s nimi.

Cieľ:
Implementovať webový nástroj na kontrolu úpravy formúl do klauzálnych teórií a kontrolu tvorby rezolvenčných dôkazov v logike prvého rádu.

Literatúra:
Genesereth, M., Kao, E.: Introduction to Logic. Third Edition. Morgan & Claypool, 2017.
Nyitraiová, A.: Educational tools for first order logic. Bakalárska práca – Univerzita Komenského, Bratislava, 2018.
Onódy, Z.: A proof assistant for first-order logic. Bakalárska práca – Univerzita Komenského, Bratislava, 2018.

Kľúčové slová:
rezolvencia, unifikácia, skolemizácia, webová aplikácia na strane klienta, nástroj na podporu výučby

Vedúci: Mgr. Ján Kľuka, PhD.
Konzultant: RNDr. Jozef Šiška, PhD.
Katedra: FMFI.KAI - Katedra aplikovanej informatiky

Prezentácia zdrojov: Stiahnuť

Finálna prezentácia: Stiahnuť

Bakalárska práca: Stiahnuť

Časový plán:

• Október - vytvoriť webstránku, štúdium technológií
• November - zostaviť časový plán, zozbierať zdroje
• December - napísať východiskovú kapitolu, začiatok implementácie
• Január - odovzdať prototyp
• Február - implementácia a tvorba textu práce
• Marec - implementácia a tvorba textu práce
• Apríl - finálne úpravy
• Máj - odovzdať hotovú prácu

Denník:

17.2.2020 - 23.2.2020
• Implementacia komponentu Language
• Implementacia komponentu ErrorMessage
• Prepojenie modulu FMFI-UK-1-AIN-412/js-fol-parser a komponentu Language

24.2.2020 - 1.3.2020
• Podrobnejsie spracovanie vychodiskovych prac aj so screenshotmi
• Zaciatok spisovania poziadaviek systemu
• Zmena implementacie generatorov pre rezolvenciu a faktorizaciu

2.3.2020 - 8.3.2020
• Vizualna uprava komponentov Language a ErrorMessage
• Implementacia dodatocnych inputov pre komponent Step

9.3.2020 - 15.3.2020
• Prepojenie parsera a komponentu Step

16.3.2020 - 22.3.2020
• State refactoring - rozdelenie stavu na dva (language, steps)
• Potrebné úpravy komponentov, ktoré využívali stav
• Presunutie implementácie parsera do reducerov stavu

23.3.2020 - 29.3.2020
• Pokracovanie v refaktorizacii -> konkretne cast steps
• Uprava komponentu step -> zmena usporadania z input-group na from-row + form-group

30.3.2020 - 5.4.2020
• Upravenie inputov pre pravidla, aby obsahovali vsetky potrebne vstupne data
• Dokoncenie implementacie parsera -> konretne parseSubstitution + parseReference
• Uprava Undo/Redo -> oddelenie potrebnych akcii pomocou groupBy

6.4.2020 - 12.4.2020
• Zmena Undo pre vsetky textove inputy
• Zaciatok implementacie overovania pravidiel
• Mensie upravy v udrzavani stavu

13.4.2020 - 19.4.2020
• Pokracovanie v implementacii overovania pravidiel

20.4.2020 - 3.5.2020
• Dokoncenie overovania pravidiel
• Implementacia prepoctu referencii pri zmene krokov
• Kontrola jednoznacnosti zobrazeni
• Kontrola disjunktnosti roznych typov symbolov

4.5.2020 -
• Import / Export
• Pokracovanie v texte prace - Analyza a navrh systemu