Bakalárska práca
Vysvetľovanie chýb vo formalizačných cvičeniach v logike prvého rádu
Vedúci projektu:
Mgr. Ján Kľuka, PhD.E-mail:
jan.kluka@fmph.uniba.skAnotácia
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 minulosti sme už takýto systém vyvinuli, ale spätnú väzbu, ktorú poskytuje, významná časť študentov nevyhodnotila ako nápomocnú. V práci na túto tému by sme preskúmať a otestovať pri výučbe ďalšie možnosti poskytovania vysvetlení chýb.
Cieľ
Cieľ
Navrhnúť a implementovať do existujúcej aplikácie na kontrolu formalizačných cvičení:
- zoskupovanie chybných riešení na základe ekvivalencie alebo ďalších relácií podobnosti medzi nimi navzájom a s očakávaným riešením;
- niekoľko techník na vysvetľovanie chýb a poskytovanie návodov na ich opravu;
- používateľské rozhranie pre učiteľov na zadávanie vstupov pre vysvetľovanie chýb a návody na opravu;
- používateľské rozhranie alebo iné mechanizmy na získavanie spätnej väzby od študentov na užitočnosť vysvetlení a návodov.
Vyhodnotiť užitočnosť vysvetlení a návodov vo výučbe.
Plán
Plán
od | do | úloha |
---|---|---|
október | január | Refaktoring predošlého kódu. |
január | marec | Zoskupiť zlé riešenia na základe ekvivalencie. Pridať používateľské rozhranie pre vyučujúceho na zadávanie feedbacku k zlým riešeniam a pre študenta na zobrazenie feedbacku s možnosťou ohodnotiť jeho užitočnosť. |
marec | apríl | Pridať používateľské rozhranie pre študenta na zobrazenie feedbacku s možnosťou ohodnotiť jeho užitočnosť. Pripraviť aplikáciu na spustenie do prevádzky. |
Denník
Denník
od | do | popis |
---|---|---|
október | december | Oboznámenie sa s predchádzajúcimi bakalárskymi prácami. Preštudovanie práce s frameworkom React, Redux, Express a dokazovačom Vampire. Refaktoring kódu. Drobné zmeny v kóde ako úprava routovania. |
január | január | Pridanie používateľského rozhrania pre študenta, na zobrazovanie jeho progresu v riešení cvičenia. |
1. február | 14. február | Zoskupenie zlých riešení na základe ekvivalencie. Pridanie migračného SQL skriptu. |
14. február | 20. február | Pridanie spätnej analýzy riešení, kedy sa zlé ekvivalentńe riešenia rozskupia. Pridanie používateľského rozhrania pre vyučujúceho, na zobrazenie chybných riešení (I.). |
20. február | 27. február | Pridanie používateľského rozhrania pre vyučujúceho, na zobrazenie chybných riešení (II.) . |
27. február | 6. marec | Spracovanie dát z minulého roka. Refaktoring migračného skriptu. Pridanie používateľského rozhrania pre vyučujúceho, na vloženie feedbacku k chybných riešeniam. |
6. marec | 15. marec | Pridanie zobrazenia počtu študentov, ktorí spravili chybu pri riešení cvičenia, tvrdenia. Pridanie funkcie na vkladanie feedbacku. Úprava zobrazenia chybných riešení a feedbackov. Pridanie používateľského rozhrania pre študenta, na zobrazenie feedbackov od učiteľa s možnosťou ohodnotiť ich nápomocnosť. |
15. marec | 20. marec | Oboznámenie sa s RTK Query. Prvotná implementácia fetchovania dát pomocou RTK Query. Zatiaľ implementované pri načítavaní zoznamu chybných cvičení a chybných tvrdení (t.j. cvičení, resp. tvrdení kde žiaci urobili aspoň jednu chybu). Písanie bakalárskej práce. |
20. marec | 3. apríl | Doimplementovanie RTK Query pri fetchovaní dát na zobrazovanie chybných riešení, a pri načítavaní dát na riešenie cvičenia. Písanie bakalárskej práce. |
3. apríl | 17. apríl | Pridanie používateľského rozhrania pre študenta, na zobrazenie feedbackov od učiteľa k chybnému riešeniu, s možnosťou ohodnotiť ich nápomocnosť. Písanie bakalárskej práce. |
17. apríl | 24. apríl | Pri zobrazení študentského progresu sa zobrazuje kedy si daný študent zobrazil aké feedbacky. Písanie bakalárskej práce. |
24. apríl | 2. máj | Nasadenie aplikácie do prevádzky, testovanie študentami. Písanie bakalárskej práce. |
Zdroje
Zdroje
- Samantha Gombárová. 2021. Automatizácia kontroly formalizačných cvičení v logike prvého rádu
- Nikola Kulíková. 2022. Automatická spätná väzba na riešenia formalizačných cvičení