Na tejto stránke nájdete interaktívne nástroje, ktoré vám pomôžu pri štúdiu teórie typov, λ-kalkulu, formálneho dokazovania a príprave technickej dokumentácie.
Viaceré z uvedených aplikácií vznikli na Katedre počítačov a informatiky FEI TUKE v rámci bakalárskych a diplomových prác.
Interaktívne dokazovanie
Rocq Game
Rocq Game je interaktívna webová aplikácia na výučbu formálneho dokazovania v systéme Rocq. Umožňuje precvičovať prácu s dôkazovými taktikami a postupne si osvojiť základné princípy konštrukcie formálnych dôkazov.
Úlohy sú organizované do tematických svetov a úrovní. Každá úroveň obsahuje tvrdenie, ktoré je potrebné dokázať pomocou systému Rocq. Aplikácia poskytuje okamžitú spätnú väzbu a umožňuje sledovať pokrok pri riešení úloh.
Vďaka integrácii jsCoq prebieha dokazovanie priamo vo webovom prehliadači bez potreby lokálnej inštalácie systému Rocq.
Aplikácia je vyvíjaná na KPI FEI TUKE v rámci projektu KEGA 052TUKE-4/2025 – Moderné prístupy vo vzdelávaní IT odborníkov v oblasti teórie typov.
Vizualizácia typových systémov a λ-kalkulu
Interaktívna typová kontrola jednoducho typovaného λ-kalkulu
Webová aplikácia umožňuje skúmať typovanie termov jednoducho typovaného λ-kalkulu (STLC) a jeho rozšírení.
Po zadaní termu aplikácia vykoná typovú kontrolu a zobrazí príslušný dôkazový strom. Jednotlivé kroky odvodenia možno interaktívne skúmať vrátane použitých typovacích pravidiel a typového kontextu.
Okrem základného λ-kalkulu podporuje aj vybrané rozšírenia, napríklad dvojice, súčtové typy, zoznamy, záznamy a rekurziu.
Aplikácia pomáha pochopiť, ako sa formálne typovacie pravidlá používajú pri odvodzovaní typov konkrétnych výrazov.
Otvoriť Type Theory Visualizer
Autor: Vladyslav Futrak, diplomová práca, KPI FEI TUKE.
Typová kontrola a vyhodnocovanie termov systému F
Interaktívny editor na prácu so systémom F, ktorý rozširuje jednoducho typovaný λ-kalkul o polymorfizmus.
Aplikácia umožňuje zapisovať polymorfné termy, vykonávať ich typovú kontrolu a sledovať postup ich vyhodnocovania.
Podporuje typovú abstrakciu, typovú aplikáciu a univerzálnu kvantifikáciu nad typmi. Výsledky typovej kontroly možno skúmať prostredníctvom dôkazových stromov.
Súčasťou aplikácie je aj vizualizácia redukčných krokov a možnosť exportu dôkazových stromov do LaTeXu.
Autor: Jakub Kiss, diplomová práca, KPI FEI TUKE.
Interpreter λ-kalkulu
Interaktívny nástroj na skúmanie vyhodnocovania termov λ-kalkulu. Umožňuje pracovať s λ-abstrakciami, aplikáciami a sledovať redukciu výrazov.
Je vhodný najmä na precvičovanie β-redukcie a pochopenie výpočtového správania λ-termov.
Otvoriť Lambda Calculus Interpreter
Autorka: Andrea Ferenczová, bakalárska práca, KPI FEI TUKE.
Typová rekonštrukcia jednoducho typovaného λ-kalkulu
Webová aplikácia na interaktívne skúmanie odvodzovania typov termov jednoducho typovaného λ-kalkulu.
Umožňuje sledovať vytváranie typových obmedzení a ich riešenie pomocou unifikačného algoritmu. Výsledné typové odvodenie je zobrazené vo forme dôkazového stromu.
Aplikácia je vhodná na pochopenie princípov typovej rekonštrukcie a vzťahu medzi typovacími pravidlami, typovými obmedzeniami a unifikáciou.
Autorka: Andrea Ferenczová, diplomová práca, KPI FEI TUKE.
Typová kontrola jednoducho typovaného λ-kalkulu v Elme
Webová aplikácia implementujúca typovú kontrolu termov jednoducho typovaného λ-kalkulu.
Poskytuje ďalší nástroj na precvičovanie typovacích pravidiel a skúmanie typovej správnosti λ-termov.
Aplikácia bola implementovaná vo funkcionálnom programovacom jazyku Elm.
Otvoriť Lambda Calculus TypeChecker
Autor: Richard Jurko, diplomová práca, KPI FEI TUKE.
Nástroje na tvorbu LaTeX dokumentov
LaTeX Code Generator
LaTeX Code Generator
LaTeX Code Generator je webová aplikácia na vizuálnu tvorbu štruktúr používaných v matematických, informatických a vedeckých dokumentoch.
Umožňuje vytvárať a generovať LaTeX kód pre:
- Karnaughove mapy,
- abstraktné syntaktické stromy,
- dôkazové stromy.
Používateľ môže požadovanú štruktúru zostaviť pomocou grafického rozhrania bez potreby manuálneho zapisovania celého LaTeX kódu.
Novšia verzia aplikácie umožňuje aj úpravu vygenerovaného kódu s priebežným zobrazením výsledku a využitie modelov umelej inteligencie na rozpoznávanie štruktúr z obrázkov a ich konverziu do LaTeXu.
Nástroj je vhodný pri príprave semestrálnych prác, záverečných prác a vedeckých článkov.
Dostupné verzie:
-
LaTeX Code Generator – aktuálna verzia
Rozšírená verzia aplikácie vytvorená v rámci diplomovej práce. -
LaTeX Code Generator – pôvodná verzia
Pôvodná aplikácia vytvorená v rámci bakalárskej práce.
Autor: Erik Laki, KPI FEI TUKE.
Detexify – rozpoznávanie LaTeX symbolov
Detexify pomáha vyhľadávať LaTeX príkazy pre matematické a iné špeciálne symboly.
Stačí nakresliť požadovaný symbol a aplikácia navrhne zodpovedajúce LaTeX príkazy vrátane informácií o potrebných balíkoch.
Nástroj je užitočný najmä pri zapisovaní matematických vzorcov a formálnych pravidiel.