Školiteľ : Mgr. Ján Kľuka, PhD.
Autor: Nikola Kulíková

SK : Automatizácia kontroly formalizačných cvičení v logike prvého rádu

EN : Automated checking of formalisation exercises in first-order logic

Formalizácia patrí k najnáročnejším témam pri výučbe logiky. Jej cieľom je čo najpresnejšie zachytiť význam neformálneho tvrdenia v prirodzenom jazyku pomocou obmedzených prostriedkov formálneho jazyka. Výučba formalizácie sa podobá výučbe cudzieho jazyka. Na jej zvládnutie je potrebné spraviť množstvo cvičení a dostať na ne spätnú väzbu. Ideálne je, keď v prípade nesprávneho či neadekvátneho riešenia spätná väzba objasní, prečo študentovo riešenie nie je vhodné – napríklad formou kontrapríkladu. Poskytovať adekvátnu a promptnú spätnú väzbu v rozsahu, aký by niektorí študenti potrebovali, často nie je v silách učiteľov.
Hoci vo všeobecnosti formalizácia nemá jednoznačné riešenie, cvičenia na túto tému sa spravidla volia tak, aby boli čo najjednoznačnejšie a kombinovali známe štandardné idiómy. Navyše sú zvyčajne výsledkom formalizácie relatívne jednoduché formuly. Relatívna jednoduchosť a jednoznačnosť riešení poskytuje príležitosť využiť na kontrolu a poskytovanie spätnej väzby existujúce dokazovače pre logiku prvého rádu. V práci na túto tému by sme tento prístup chceli bližšie preskúmať, implementovať a otestovať pri výučbe.

• Vytvoriť webovú službu na overovanie správnosti formalizácie voči vhodne uloženému očakávanému riešeniu alebo riešeniam a generovanie kontrapríkladov neočakávaných riešení.
• Doplniť službu vhodným používateľským rozhraním pre študentov aj učiteľov.
• Otestovať aplikáciu pri výučbe a preskúmať možnosti generovania a prezentácie kontrapríkladov vzhľadom na zrozumiteľnosť.
• Integrovať rozhranie do interaktívneho pracovného zošitu vytvoreného v paralelnej bakalárskej práci a integrovať autentifikáciu s portálom GitHub používaným pri výučbe.