Školiteľ : Mgr. Ján Kľuka, PhD.
Autor: Nikola Kulíková
Názov
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
Anotácia
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.
Cieľ
• 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.