Je interaktívny dokazovací systém vyvinutý pre potreby výučby. V aktuálnej verzii obsahuje sadu 44 úloh na precvičenie formálnych dôkazov využitím prirodzenej dedukcie vo výrokovej a predikátovej logike. Používateľské rozhranie poskytuje spätnú väzbu priamo v rámci procesu dokazovania na základe chybových hlásení. Základnou filozofiou nástroja je podporovať študentov, pričom verne emuluje proces tvorby dôkazov tak, akoby pracovali na papieri.
Tento nástroj sme vyvinuli v spolupráci s Univerzitou v Osle v rámci projektu "Moderný prístup k výučbe predmetov na univerzitnej úrovni v oblasti teoretickej informatiky.", ktorý bol podporený Islandom, Lichtenštajnskom a Nórskom prostredníctvom grantov EHP a Nórskych grantov, iniciatívou č.: FBR-PDI-025.
Rocq Game
Rocq Game je interaktívna webová aplikácia, ktorej cieľom je uľahčiť študentom prácu s interaktívnym dokazovacím systém Rocq.
Táto aplikácia bolo vyvinutá v rámci projektu KEGA: "052TUKE-4/2025" "Moderné prístupy vo vzdelávaní IT odborníkov v oblasti Teórie typov", spoločne s pánom Khaledom Jamalom Sulimanom.
Typografický systém $\LaTeX$
Generátor kódu typografického systému $\LaTeX$
umožňuje generovanie kódu z webovej aplikácie prostredníctvom používateľsky priateľského UI pre:
Pôvodná verzia tejto aplikácie bola vyvinutá v rámci bakalárskej práce Erika Lakiho, ktorý ju následne rozšíril o ďalšie funkcie a vylepšil používateľské rozhranie.
https://ero67.github.io/latex-code-generator/
Detekcia špeciálnych symbolov
Táto webová aplikácia deteguje nakreslený symbol a vráti $\LaTeX$ príkaz ako aj potrebný balíček.
