|
|
Formální popis deskových her
Nowak, Stanislav ; Štěpánek, Petr (vedoucí práce) ; Kunčar, Ondřej (oponent)
Cílem bakalářské práce bylo navrhnout matematický formalismus umožňující popis a zkoumání vlastností deskových her. Práce těží především z poznatků teorie automatů a logického programování. Z teorie automatů se práce zabývá konečnými automaty a jejich možnou aplikací pro potřeby deskových her. Výsledkem je rozšíření konečného automatu pokrývající specifika deskových her nazvané herní automat. Deskové hry jsou komplexní doménou a nabízí se využít k jejich popisu prostředků vyšší úrovně. Takovým prostředkem je i logické programovaní. S využitím logického programování byl navržen nástroj, který umožňuje deklarativní popis her, pojmenovaný herní systém. Tento deklarativní popis tvoří rámec pro implementaci interaktivních her. Propojení obou světů bude demonstrováno převodem herního systému na herní automat.
|
|
|
Systémy pro formální matematiku
Kunčar, Ondřej ; Urban, Josef (vedoucí práce) ; Štěpánek, Petr (oponent)
Typový systeé Mizaru je pomrěně sofistikovaný - obsahuje celou řadu vlastností, jako jsou závislé typy, atributy, přetěžování, konstrukci podtypů, struktury a další. Tyto vlastnosti nemalou měrou přispívají k tomu, že formalizace matematiky je v systému Mizar mnohem intuitivnější než v ostatních systé'mech. Zároveň vyvstává potřeba verifikovat matematické poznatky formalizované v Mizaru i v jiných systémech, aby se zvýšla jistota, že systém Mizar pracuje korektně. Je tedy přirozené pokusit se rekonstruovat tento typový systém v jiných systémech pro formalizaci matematiky. Tato práce navrhuje takovou rekonstrukci do systému HOL Light. Idea rekonstrukce je reprezentovat typy Mizaru jako predikáty v tomto systému (HOL Light). Součástí této práce je i pokus o co nejpřesnější zachycení relevantní části typového systému Mizaru. V závěru jsou pak uvedeny postřehy, které byly učiněny při návrhu a částecné implementaci navržené rekonstrukce.
|
|
|
Systémy pro formální matematiku
Kunčar, Ondřej ; Urban, Josef (vedoucí práce) ; Štěpánek, Petr (oponent)
Na'zev pra'ce: Syste'my pro forma'lnı' matematiku Autor: Ondrěj Kuncˇar Katedra (u'stav): Katedra teoreticke' informatiky a matematicke' logiky Vedoucı' diplomove' pra'ce: Mgr. Josef Urban, Ph.D. e-mail vedoucı'ho: josef.urban@gmail.com Abstrakt: Typovy' syste'm Mizaru je pomeřneˇ sofistikovany' - obsahuje celou rˇadu vlastnostı', jako jsou za'visle' typy, atributy, prětežˇova'nı', konstrukci podtypu˚, struktury a dalsˇı'. Tyto vlastnosti nemalou meřou prˇispı'vajı' k tomu, zě forma- lizace matematiky je v syste'mu Mizar mnohem intuitivneˇjsˇı' nezˇ v ostatnı'ch syste'mech. Za'rovenˇ vyvsta'va' potrěba verifikovat matematicke' poznatky forma- lizovane' v Mizaru i v jiny'ch syste'mech, aby se zvy'sˇila jistota, zě syste'm Mizar pracuje korektneˇ. Je tedy prˇirozene' pokusit se rekonstruovat tento typovy' syste'm v jiny'ch syste'mech pro formalizaci matematiky. Tato pra'ce navrhuje takovou rekonstrukci do syste'mu HOL Light. Idea rekon- strukce je reprezentovat typy Mizaru jako predika'ty v tomto syste'mu (HOL Light). Soucˇa'stı' te'to pra'ce je i pokus o co nejprěsneˇjsˇı' zachycenı' relevantnı' cˇa'sti typove'ho syste'mu Mizaru. V za'veřu jsou pak uvedeny postrěhy, ktere' byly ucˇi- neňy prˇi na'vrhu a cˇa'stecňe' implementaci navrzěne' rekonstrukce. Klı'cˇova' slova: typovy' syste'm, Mizar, HOL...
|
|
|
Formální popis deskových her
Nowak, Stanislav ; Štěpánek, Petr (vedoucí práce) ; Kunčar, Ondřej (oponent)
Cílem bakalářské práce bylo navrhnout matematický formalismus umožňující popis a zkoumání vlastností deskových her. Práce těží především z poznatků teorie automatů a logického programování. Z teorie automatů se práce zabývá konečnými automaty a jejich možnou aplikací pro potřeby deskových her. Výsledkem je rozšíření konečného automatu pokrývající specifika deskových her nazvané herní automat. Deskové hry jsou komplexní doménou a nabízí se využít k jejich popisu prostředků vyšší úrovně. Takovým prostředkem je i logické programovaní. S využitím logického programování byl navržen nástroj, který umožňuje deklarativní popis her, pojmenovaný herní systém. Tento deklarativní popis tvoří rámec pro implementaci interaktivních her. Propojení obou světů bude demonstrováno převodem herního systému na herní automat.
|
|
|
Systémy pro formální matematiku
Kunčar, Ondřej ; Urban, Josef (vedoucí práce) ; Štěpánek, Petr (oponent)
Na'zev pra'ce: Syste'my pro forma'lnı' matematiku Autor: Ondrěj Kuncˇar Katedra (u'stav): Katedra teoreticke' informatiky a matematicke' logiky Vedoucı' diplomove' pra'ce: Mgr. Josef Urban, Ph.D. e-mail vedoucı'ho: josef.urban@gmail.com Abstrakt: Typovy' syste'm Mizaru je pomeřneˇ sofistikovany' - obsahuje celou rˇadu vlastnostı', jako jsou za'visle' typy, atributy, prětežˇova'nı', konstrukci podtypu˚, struktury a dalsˇı'. Tyto vlastnosti nemalou meřou prˇispı'vajı' k tomu, zě forma- lizace matematiky je v syste'mu Mizar mnohem intuitivneˇjsˇı' nezˇ v ostatnı'ch syste'mech. Za'rovenˇ vyvsta'va' potrěba verifikovat matematicke' poznatky forma- lizovane' v Mizaru i v jiny'ch syste'mech, aby se zvy'sˇila jistota, zě syste'm Mizar pracuje korektneˇ. Je tedy prˇirozene' pokusit se rekonstruovat tento typovy' syste'm v jiny'ch syste'mech pro formalizaci matematiky. Tato pra'ce navrhuje takovou rekonstrukci do syste'mu HOL Light. Idea rekon- strukce je reprezentovat typy Mizaru jako predika'ty v tomto syste'mu (HOL Light). Soucˇa'stı' te'to pra'ce je i pokus o co nejprěsneˇjsˇı' zachycenı' relevantnı' cˇa'sti typove'ho syste'mu Mizaru. V za'veřu jsou pak uvedeny postrěhy, ktere' byly ucˇi- neňy prˇi na'vrhu a cˇa'stecňe' implementaci navrzěne' rekonstrukce. Klı'cˇova' slova: typovy' syste'm, Mizar, HOL...
|
|
|
Systémy pro formální matematiku
Kunčar, Ondřej ; Štěpánek, Petr (oponent) ; Urban, Josef (vedoucí práce)
Typový systeé Mizaru je pomrěně sofistikovaný - obsahuje celou řadu vlastností, jako jsou závislé typy, atributy, přetěžování, konstrukci podtypů, struktury a další. Tyto vlastnosti nemalou měrou přispívají k tomu, že formalizace matematiky je v systému Mizar mnohem intuitivnější než v ostatních systé'mech. Zároveň vyvstává potřeba verifikovat matematické poznatky formalizované v Mizaru i v jiných systémech, aby se zvýšla jistota, že systém Mizar pracuje korektně. Je tedy přirozené pokusit se rekonstruovat tento typový systém v jiných systémech pro formalizaci matematiky. Tato práce navrhuje takovou rekonstrukci do systému HOL Light. Idea rekonstrukce je reprezentovat typy Mizaru jako predikáty v tomto systému (HOL Light). Součástí této práce je i pokus o co nejpřesnější zachycení relevantní části typového systému Mizaru. V závěru jsou pak uvedeny postřehy, které byly učiněny při návrhu a částecné implementaci navržené rekonstrukce.
|
|
|
SVN Proxy
Kunčar, Ondřej ; Galamboš, Leo (oponent) ; Bednárek, David (vedoucí práce)
SVN Proxy je aplikace, která se chová jako proxy SVN repository. Obsahuje lokální repository, do kterého uživatel provádí commity. Lokální repository je schopné se na požádání synchronizovat se vzdáleným SVN repository. Lokální revizemohou být číslovány tak, aby nedošlo k rozsynchronizování číslování se vzdáleným repository. Data v lokálním repository jsou ukládána v jazyku XML. Program obsahuje implementaci hledání rozdílů mezi verzemi a umí verze spojovat a detekovat konflikty. SVN Proxy je aplikace pro příkazovou řádku a její rozhraní je odvozeno z rozhraní standardního SVN klienta. V návrhu aplikace je kladen důraz na snadnost budoucího rozvoje. Návrh umožňuje přidání dalších přístupových metod k repository a vytvoření jiných uživatelských rozhraní včetně GUI. Aplikace je určena pro vývojáře zdrojových textů, kteří nechtějí nebo nemohou posílat kažý commit do vzdáleného repository.
|
host ::
RSS.