|
|
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.
|
|
|
REDUKCE DYNAMIKY SIGNÁLU V SYSTÉMECH S ORTOGONÁLNÍM FREKVENČNÍM MULTIPLEXEM
Urban, Josef ; Lúč, Andrej (oponent) ; Galajda,, Pavol (oponent) ; Maršálek, Roman (vedoucí práce)
Předložená dizertační práce je zaměřená do oblasti radiových komunikačních systému s více nosnými. Tyto systémy jsou perspektivní pro současné i budoucí systémy v mobilních komunikacích a bezdrátových sítích. Výhody použití více nosných jako jsou například odolnost vůči mnohacestnému šíření jsou vykoupeny i některými nevýhodami. Mezi ty patří zejména velký poměr mezi špičkovým a středním výkonem přenášeného signálu, který je překážkou v provozu výkonových zesilovačů v pásmu vysoké účinnosti. Práce se zabývá metodami redukce poměru mezi špičkovým a středím výkonem pro systémy OFDM, které jsou jedněmi z nejvyužívanějších systémů s více nosnými. Jedním z hlavních cílů je modifikace stávajících metod vedoucí ke snížení výpočetní náročnosti. Předmětem zájmu je dále analýza možností vzájemných kombinací vhodných metod vedoucích k výraznějšímu snížení poměru mezi špičkovým a středním výkonem bez nežádoucího zvýšení chybovosti. Součástí je také studium vlivu těchto metod na OFDM signály s různými parametry.
|
|
|
Modulátor a demodulátor s více nosnými pro softwarově definované rádio
Klučka, Jaroslav ; Urban, Josef (oponent) ; Maršálek, Roman (vedoucí práce)
Diplomová práce se zabývá počítačovou simulací komunikačního řetězce s použitím OFDM modulace. V úvodu práce je stručný popis digitálních modulací, zejména OFDM. V prostředí MATLAB je navržen a simulován model vysílače, rádiového kanálu a přijímače, včetně jednoduché časové a frekvenční synchronizace a ekvalizace. V prostředí Simulink je navržený komunikační systém implementován do vývojového kitu USRP. Nebylo možné, aby vývojový kit pracoval zároveň jako vysílač i jako přijímač. Funkce vysílače byla ověřena měřením na spektrálním analyzátoru. Pro ověření funkce přijímače byl vygenerován zkušební OFDM signál pomocí vzorkovací karty CompuGen 4302. Na vývojovém kitu pracujícím jako přijímač byl signál přijat a demodulován.
|
|
|
Implementace OFDM demodulátoru v obvodu FPGA
Solar, Pavel ; Urban, Josef (oponent) ; Maršálek, Roman (vedoucí práce)
Diplomová práce stručně rozebírá princip OFDM modulace, možnosti synchronizace a odhadu frekvenční charakteristiky kanálu v OFDM. Je vytvořen jednoduchý model OFDM systému v programu MATLAB. Kombinací schématického popisu a popisu v jazyce VHDL je vytvořen ve vývojovém prostředí ISE behaviorální popis OFDM demodulátoru pro implementaci do FPGA.
|
|
|
Redukce PAPR v OFDM a její simulace ve Scilabu
Maňák, David ; Maršálek, Roman (oponent) ; Urban, Josef (vedoucí práce)
Cílem této práce je prostudování modulace OFDM její princip a vlastnosti. Dále se seznámíme s vybranými základními metodami pro redukci dynamiky PAPR v OFDM, jako např. ořezávání signálu (Clipping) nebo prokládání vstupní posloupnosti bitů (Interleaving). Simulace metod redukce bude probíhat v prostředí Scilab, kde jsou vytvořeny základní funkce pro modulátor a demodulátor modulace OFDM. Dále jsou vytvořeny funkce pro metody redukce PAPR. Všechny vytvořené funkce jsou implementovány do GUI.
|
|
|
GSM alarm pro motocykly
Beníček, Martin ; Fedra, Zbyněk (oponent) ; Urban, Josef (vedoucí práce)
Cílem této diplomové práce je navrhnout a realizovat spolehlivé zabezpečovací zařízení na motocykly za použití technologie GSM. V práci se budu věnovat jednotlivým oblastem, kterými jsem prošel během návrhu aplikace. V úvodní kapitole se čtenář seznámí s vyhodnocením předchozích semestrálních projektů a se stručným popisem realizovaného zařízení. Dále jsou popsány principy komunikace mezi mikropočítačem a mobilním telefonem. Hlavní část je věnována návrhu samotné aplikace motoalarmu. Poslední kapitola obsahuje popis služby Kde je…, která slouží k lokalizaci mobilního telefonu. V závěru je pak vyhodnocení práce a souhrnný popis realizovaného zařízení.
|
|
| |
|
|
Reakce vybraných odrůd brambor na hustotu porostu
URBAN, Josef
Cílem práce bylo zhodnotit projev čtyř hustot porostu u vybraných odrůd brambor. Práce obsahuje založení pokusu se 4 odrůdami brambor. Zvolena byla standardní technologie pěstování konzumních brambor. Zvolené hustoty porostu byly 35, 40, 45 a 50 tis. jedinců.ha-1. Každá varianta měla 4 opakování. Hodnocen byl výnos hlíz, podíl a výnos konzumních hlíz, průměrný počet hlíz na rostlinu, hmotnost hlíz na rostlinu, průměrná hmotnost 1 hlízy, průměrná hmotnost konzumních hlíz. Práce byla prováděna na soukromé farmě jako polní pokus. Farma se nachází v bramborářské oblasti na Vysočině v nadmořské výšce 490 m. Brambory se zde pěstují na výměře cca 7 ha. Pokus byl založen v roce 2010. K založení byl použit sazeč brambory MARS 42 s vzdáleností řádků 0,75 m. Byly použity odrůdy Mirage, Agria, Victoria, Marabel, všechny ve stupni množení C1. Parcely se skládaly ze 4 řádků, každý řádek se rovná jednomu opakování, každá parcela se rovná jedné hustotě porostu. Při odběru vzorků byl proveden odkop 10 rostlin z každého opakování. Následovalo velikostní rozdělení hlíz v každém vzorku. Na velikost hlíz nad 40 mm a pod 40 mm. Po rozdělení byly jednotlivé vzorky zváženy a spočteny hlízy. Z hodnot počtu hlíz a hmotnosti hlíz ve vzorku se vychází při dílčích hodnocení. Z výsledků bylo zjištěno, že ve většině hodnocení dosáhla odrůda Mirage nejvhodnějších výsledků při hustotě porostu 45 000 jedinců.ha-1. Odrůda Agria měla dvě vhodné hustoty porostu, a to 40 000 a 45 000 jedinců.ha-1, mezi těmito hustotami nebyl výrazný rozdíl. Odrůda Victoria měla nejvhodnějších výsledek při hustotě porostu 35 000 jedinců.ha-1, stejně tak odrůda Marabel, která má nejvhodnější výsledek také při hustotě porostu 35 000 jedinců.ha-1. Pro všechny odrůdy se jako nevhodná jevila hustota porostu 50 000 jedinců.ha-1. Reakce odrůd na tuto hustotu porostu se projevila snížením všech hodnocených ukazatelů a také z pohledu finanční náročnosti na množství sadby, vyššímu tlaku chorob a škůdců zde dochází ke ztrátám.
|
|
|
Hodnocení sklízecích mlátiček Fendt 8350 a CLAAS Lexion 580 TERRA TRAC
URBAN, Josef
Cílem práce je hodnocení činnosti a kvality práce sklízecích mlátiček dvou výrobců při sklizni zemědělských plodin a jejich jednoduché ekonomické zhodnocení. Rozbor činnosti a kvality práce je zaměřen na velikost ztrát, vlivu vlhkosti na velikost ztrát, kvality drcení a rozmetání rostlinných zbytků. Rozmetání a drcení rostlinných zbytků a rozboru výkonností a spotřeby PHM.
|
host ::
RSS.