- Rekonstrukce typového systému Mizaru v systému HOL Light2010 | Matematicko-fyzikální fakulta
- Integrované sémantické brouzdání matematické knihovny Mizaru pro vytváření článků v Mirazu2004 | Publikace bez příslušnosti k fakultě
- Překlad Mizaru pro dokazovače v logice 1. řádu2003 | Publikace bez příslušnosti k fakultě
- MizarMode - asistant pro psani dukazu v formalnim matematickem systemu Mizar2006 | Matematicko-fyzikální fakulta
- Automatické dokazování pro Mizar: umělá inteligence pomocí výměny znalostíPublikace bez příslušnosti k fakultě
- XML-izace Mizaru: zjednodušení semantického zpracování a prezentace MML2006 | Matematicko-fyzikální fakulta
- Křížová verifikace pomocí ATP mizarovské MPTP výzvy k řešení problémů2007 | Matematicko-fyzikální fakulta
- XML-izace Mirazu: Zjednodušení sémantického zpracování a prezentace MML2006 | Publikace bez příslušnosti k fakultě
- MPTP - Motivace, implementace, první experimenty2005 | Matematicko-fyzikální fakulta
- Prostory, které jsou generovány diskrétními množinami2004 | Publikace bez příslušnosti k fakultě
- MPTP 0.2: Design, Implementace, and pocatecni experimenty2006 | Matematicko-fyzikální fakulta
- MPTP - Motivation, Implementation, First Experiments2005 | Matematicko-fyzikální fakulta
- MaLARea SG1 - Strojové učení se pro automatické dokazování se sémantickým řízením2008 | Matematicko-fyzikální fakulta
- Momm - Rychle interredukce a dotazy ve velkych knihovnach formalni matematiky2006 | Matematicko-fyzikální fakulta