|
|
Historie fotbalového klubu v Kostelci nad Labem
Urban, Josef ; Pokorný, Ladislav (vedoucí práce) ; Dlouhý, Martin (oponent)
Cílem práce bylo popsat historii fotbalového klubu v Kostelci nad Labem. Okolnosti vzniku, jeho počátky a sportovní úsilí od počátku až do dnešních dnů. Práci jsem rozdělil do dvou tématických celků: teoretického a praktického. Prvních pět kapitol je zaměřeno teoreticky, šestá prakticky. V prvních dvou kapitolách jsou stanoveny cíle, úkoly a hypotézy práce. Třetí kapitola se zabývá charakteristikou fotbalu. Ve čtvrté kapitole se věnuji historickému vývoji kopané ve světe a u nás. Pátá kapitola je nejobsáhlejší a pojednává o vzniku a historii fotbalového klubu, ve výše uvedeném městě a o jeho současné podobě a činnosti . Šestá kapitola-rozhovor s fotbalovým pamětníkem a zároveň trenérem mládeže. Tuto část považuji za nejdůležitější a použité otázky směřují k ověření, či zamítnutí stanovených hypotéz. Práce má kompilační charakter a mohla by být přínosem jak pro lidi, kteří se zabývají fotbalem, tak i pro ty, kteří by se chtěli dozvědět něco o zakládání fotbalových klubů u nás a o jejich začátcích .
|
|
|
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.
|
|
|
Formalizace relace odvoditelnosti pro výrokové fuzzy logiky
Révay, Petr ; Běhounek, Libor (vedoucí práce) ; Urban, Josef (oponent)
Tato bakalářská práce předkládá formalizaci relace odvoditelnosti fuzzy logiky BL v prostředí matematického asistenta Isabelle/HOL a počítačově ověřené důkazy některých teorémů a meta-teorémů této logiky. Zároveň poskytuje popis procesu formalizace a použité prostředky Isabelle/HOL předvádí na jednodušších příkladech. Samostatná kapitola je pak věnována úvodu do logiky BL. Po nastudování dokumentace a volbě vhodných nástrojů Isabelle/HOL byla implementována formalizace, díky níž lze v programu ověřovat důkazy jak v axiomatizaci BL, tak i důkazy vlastností relace dokazatelnosti. Z těch byl formalizován především důkaz věty o lokální dedukci. Dále byly formalizovány důkazy řady teorémů BL, a to včetně odvození redundantních axiomů BL2 a BL3. Přínosem této práce je prozkoumání možností verifikátoru Isabelle/HOL z hlediska použití pro fuzzy logiku BL. Vzhledem k uvedeným poznatkům je možné práci použít jako základ širšího projektu formalizace fuzzy logik, které z logiky BL vycházejí. Powered by TCPDF (www.tcpdf.org)
|
|
|
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...
|
|
|
Neural modelling of mathematical structures and their extensions
Smolík, Martin ; Urban, Josef (vedoucí práce) ; Holub, Štěpán (oponent)
V tejto práci sa snažíme vybudovať algebraické modely v počítači použitím strojového učenia, konkrétne neurónových sietí. Začneme množinou axiómov ktoré popisujú funkcie, konštanty a relácie a použijeme ich na trénovanie neurónových sietí ktoré ich aproximujú. Každý prvok je reprezentovaný reálnym vektorom, aby na nich neurónové siete mohli operovať. Taktiež skúmame a porovnávame rôzne reprezentácie. Táto práca sa zaoberá hlavne grupami. Trénujeme neurónové reprezentácie pre cyklické (najjednoduchšie) a symetrické (najkomplikovanejšie) grupy. Ďalšou časťou tejto práce sú experimenty s rozšírením týchto natrénovaných modelov pomocou "alge- braických" prvkov, podobne ako klasické rozšírenia racionálnych čísel, napr. Q[ √ 2]. 1
|
|
|
Neural modelling of mathematical structures and their extensions
Smolík, Martin ; Urban, Josef (vedoucí práce) ; Holub, Štěpán (oponent)
V tejto práci sa snažíme vybudovať algebraické modely v počítači použitím strojového učenia, konkrétne neurónových sietí. Začneme množinou axiómov ktoré popisujú funkcie, konštanty a relácie a použijeme ich na trénovanie neurónových sietí ktoré ich aproximujú. Každý prvok je reprezentovaný reálnym vektorom, aby na nich neurónové siete mohli operovať. Taktiež skúmame a porovnávame rôzne reprezentácie. Táto práca sa zaoberá hlavne grupami. Trénujeme neurónové reprezentácie pre cyklické (najjednoduchšie) a symetrické (najkomplikovanejšie) grupy. Ďalšou časťou tejto práce sú experimenty s rozšírením týchto natrénovaných modelov pomocou "alge- braických" prvkov, podobne ako klasické rozšírenia racionálnych čísel, napr. Q[ √ 2]. 1
|
|
|
Mapování historických objektů malých pivovarů v příhraničním regionu
URBAN, Josef
Historické pivovary byly nedílnou součástí majetku významných rodů a sloužily jako jeden z důležitých finančních zdrojů. Tato práce zpracovává historická fakta od středověku až po současnost týkající se jednotlivých pivovarů v obcích a městech na Českokrumlovsku. Zabývá se základními i obecnými informacemi týkajících se roku založení, základní historickou charakteristikou, roční výstavou a rokem, kdy byl provoz pivovaru ukončen. Zpracována je také bodová mapa jednotlivých pivovarů dle majitele a přehledná tabulka s nejdůležitějšími údaji.
|
|
|
Formalizace relace odvoditelnosti pro výrokové fuzzy logiky
Révay, Petr ; Běhounek, Libor (vedoucí práce) ; Urban, Josef (oponent)
Tato bakalářská práce předkládá formalizaci relace odvoditelnosti fuzzy logiky BL v prostředí matematického asistenta Isabelle/HOL a počítačově ověřené důkazy některých teorémů a meta-teorémů této logiky. Zároveň poskytuje popis procesu formalizace a použité prostředky Isabelle/HOL předvádí na jednodušších příkladech. Samostatná kapitola je pak věnována úvodu do logiky BL. Po nastudování dokumentace a volbě vhodných nástrojů Isabelle/HOL byla implementována formalizace, díky níž lze v programu ověřovat důkazy jak v axiomatizaci BL, tak i důkazy vlastností relace dokazatelnosti. Z těch byl formalizován především důkaz věty o lokální dedukci. Dále byly formalizovány důkazy řady teorémů BL, a to včetně odvození redundantních axiomů BL2 a BL3. Přínosem této práce je prozkoumání možností verifikátoru Isabelle/HOL z hlediska použití pro fuzzy logiku BL. Vzhledem k uvedeným poznatkům je možné práci použít jako základ širšího projektu formalizace fuzzy logik, které z logiky BL vycházejí. Powered by TCPDF (www.tcpdf.org)
|
|
|
Lucemburkové a Apeninský poloostrov
Urban, Josef ; Helan, Pavel (vedoucí práce) ; Lášek, Jan Blahoslav (oponent)
Diplomová práce Lucemburkové a Apeninský poloostrov se zabývá působením rodu Lucemburků v Itálii v první třetině 14. století, konkrétně v letech 1308-1313, 1330- 1333 a roku 1337. Podává stručný přehled vzniku a vývoje Lucemburské dynastie do čtrnáctého století včetně neklidné politické situace v Evropě po smrti Albrechta I. Habsburského a volby Jindřicha IV, římským králem. Především se však zaměřuje na postup Jindřicha IV. za císařskou korunou a snahy Jana Lucemburského a Karla Lucemburského o založení lucemburské signorie na území Lombardie, Toskánska a Emilia Romagna. Pokouší se postihnout charakter jejich činnosti na poloostrově a vliv jejich politického působení na konstituci městských států a komun. Dále obsahuje exkurz do politické situace Apeninského poloostrova na počátku 14. století. Také se stručně věnuje vlivu Jindřicha Lucemburského na spisovatele Danta Alighieriho v kontextu jeho filosofického traktátu "De Monarchia". V závěru se pokouším alespoň stručně porovnat charakter působení Jindřicha VII. Jana Lucemburského a Karla Lucemburského v jeho mládí, na Apeninském poloostrově. Cílem práce je postihnout italské události, které stály za posílením a rozkvětem Lucemburské dynastie.
|
|
|
Historie fotbalového klubu v Kostelci nad Labem
Urban, Josef ; Pokorný, Ladislav (vedoucí práce) ; Dlouhý, Martin (oponent)
Cílem práce bylo popsat historii fotbalového klubu v Kostelci nad Labem. Okolnosti vzniku, jeho počátky a sportovní úsilí od počátku až do dnešních dnů. Práci jsem rozdělil do dvou tématických celků: teoretického a praktického. Prvních pět kapitol je zaměřeno teoreticky, šestá prakticky. V prvních dvou kapitolách jsou stanoveny cíle, úkoly a hypotézy práce. Třetí kapitola se zabývá charakteristikou fotbalu. Ve čtvrté kapitole se věnuji historickému vývoji kopané ve světe a u nás. Pátá kapitola je nejobsáhlejší a pojednává o vzniku a historii fotbalového klubu, ve výše uvedeném městě a o jeho současné podobě a činnosti . Šestá kapitola-rozhovor s fotbalovým pamětníkem a zároveň trenérem mládeže. Tuto část považuji za nejdůležitější a použité otázky směřují k ověření, či zamítnutí stanovených hypotéz. Práce má kompilační charakter a mohla by být přínosem jak pro lidi, kteří se zabývají fotbalem, tak i pro ty, kteří by se chtěli dozvědět něco o zakládání fotbalových klubů u nás a o jejich začátcích .
|
host ::
RSS.