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.
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:
