Abstrakt
Systém Mizar je systém pro formalizaci matematiky. Obsahuje poměrně složitý a bohatý typový systém, ve kterém je formalizace matematiky v Mizaru intuitivnější než v jiných systémech.
Na druhou stranu, typový systém Mizaru je velmi složitý a společně s neprůhlednou implementací verifikátoru Mizaru panují obavy o správnost systému Mizar. Jedním z možných řešení je přeložit Matematickou kinihovnu Mizaru (MML) do jiného systému pro formalizaci matematiky a referifikovat MML v něm.
HOL Light je systém, který byl pro tento účel vybrán a prvním nezbytným krokem navrhovaného překladu je rekonstruce typového systému Mizaru v systému HOL Light, což je cílem předkládané práce. Rekonstrukce není jednoduché z důvodu složitosti typového systému Mizaru a z důvodu různých druhů logik použitých v obou systémech (logika prvního řádu versus logika vyššího řádu).
Základní myšlenkou je reprezentovat typy Mizaru jako predikáty a vyjádřit dynamickou část systému typového systému jako dokázané teorémy v systému HOL Light.