|
|
Simulace obchodování na akciovém trhu
Ulrych, Stanislav ; Jakob, Michal (oponent) ; Štěpánek, Petr (vedoucí práce)
Tato diplomová práce se zabývá simulací obchodování na elektronickém akciovém trhu NASDAQ. Soustředí se na simulaci obchodování s vysokou frekvencí, tzv. High Frequency Trading (HFT) strategií. Simulace je založena na sloučení skutečných historických order flow dat s daty produkovanými simulovanými HFT strategiemi, což je koncept, který zatím nebyl dostatečně zkoumán. Práce se věnuje problémům spojeným s věrohodnou simulací na základě order flow dat, mezi něž patří zpracování order flow dat, přesné časové zpracování, parametrické zpoždění obchodních signálů, specifika různých typů obchodních příkazů aj. Součástí práce je také návrh postupu simulace a jeho implementace s ohledem na vysokou výpočetní náročnost, modularizovatelnost jednotlivých strategií a paralelizovatelnost celého výpočtu. V poslední části práce je také předvedena implementace a výsledky testování jednoduché HFT strategie.
|
|
|
Koordinace mezi logickými agenty
Krištofič, Milutín ; Vojtáš, Peter (oponent) ; Štěpánek, Petr (vedoucí práce)
V predloženej práci študujeme súčasné modely pre koordináciu a navrhujeme nový model založený na argumentačnom systéme. Tento systém, nazvaný Argumentation BlackBoard for Coordination (ABBC) a jeho rozšírenie, Abstract ABBC, zakladáme na úspešných argumentačných prístupoch ako je abstraktný argumentačný framework a defeasible logic programming. Náš hlavný zámer je zachytenie potrebných argumentačných zložiek v otvorenom multi-agentnom systéme s logickými agentami. V práci je popisaný aj stručný návrh na implementáciu takého systému.
|
|
|
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.
|
|
|
Metafory a modelování živých systémů
Ibrahimová, Nora ; Štěpánek, Petr (oponent) ; Havel, Ivan (vedoucí práce)
Předložená práce si klade za cíl teoreticky prozkoumat a popsat některé modely živých systémů. V první části se zabývá modely autonomních systémů, jako je například buňka nebo živý tvor jako celek. V této části je představen princip autopoieze a matematický model autopoietického systému. Kromě toho jsou zde prozkoumány další související, filosofi cky relevantní pojmy a principy. Druhá část podrobně popisuje a srovnává dva dynamické modely mozku. Obě části se přitom nesou v duchu tzv. enaktivního přístupu, kladou důraz na dynamiku a využívají znalostí a pojmů z teorie dynamických systémů. Součástí práce je i vytvoření modelu jednoho z klíčových pojmů - senzomotoriky - pomocí neuronové sítě.
|
|
| |
|
|
eHealth: nová média ve zdravotnictví
Bartůňková, Lucie ; Štěpánek, Petr (vedoucí práce) ; Šlerka, Josef (oponent)
Práce mapuje možnosti využití nových médií v oblasti zdravotnictví. Jsou zde představeny české i zahraniční projekty využívající mobilní technologie, internet a televizní a rozhlasové vysílání ke zlepšení komunikace mezi lékaři i mezi lékařem a pacientem, a také ke zvýšení informovanosti veřejnosti o zdravotnických tématech. V úvodní části jsou vysvětleny hlavní pojmy práce - eHealth a nová média. V dalších kapitolách jsou jednotlivá média představena a následuje výběr konkrétních zdravotnických projektů. Závěrečná kapitola je věnována využívání nových médií v komunikaci mezi lékařem a pacientem v České republice a vychází z dotazníkového průzkumu na toto téma.
|
|
|
Mediální výchova v České republice s důrazem na nová média
Marková, Anna ; Štěpánek, Petr (vedoucí práce) ; Štogr, Jakub (oponent)
Práce se zaměřuje na problematiku mediální gramotnosti v rozvíjející se informační společnosti. Vymezuje význam nových médií a nutnost zprostředkovávat dovednosti a schopnosti potřebné pro jejich používání. Definuje tento soubor kompetencí, který zajišťuje efektivní používání informačních, komunikačních a zábavních možností nových médií. Přitom práce vychází především z poznatků teorie a praxe mediální výchovy ve Spolkové republice Německo. Práce dále nastiňuje stav mediální výchovy zaměřené na nová v České republice. Uvedeny jsou příklady projektů z oblasti mediální výchovy zaměřené na nová média realizovaných ve Spolkové republice Německo. Závěrem práce nabízí metodické tipy pro pedagogické zpracování problematiky nových médií ve školství České republiky.
|
|
|
Verefication of Mathematical Proofs
Pudlák, Petr ; Štěpánek, Petr (vedoucí práce) ; Haniková, Zuzana (oponent) ; Plátek, Martin (oponent)
In this thesis we deal with the problem of automatic proving (or disproving) mathematical conjectures using computer programs (usually called automated theorem provers). We address several issues that are important for a successful utilization of such programs. In Chapter 3 we examine how to store and reuse important pieces of mathematical knowledge in the form of lemmas. We investigate how this process can be automatized, i.e. how a computer can construct and use lemmas without human guidance. The program we develop tries to shorten or to speed up the proofs of several conjectures from a common theory. It repeatedly extracts lemmas from the proofs it has already completed and uses the lemmas to improve the sets of premisses to produce more efficient proofs of the conjectures. In Chapter 4 we develop a new algorithm that tries to construct the optimal sets of premisses for proving and disproving mathematical conjectures. The algorithm semantically analyzes the conjectures and the set of premisses of the given theory to find the optimal subsets of the premisses. The algorithm uses an automated model finder to construct models that serve as counterexamples that guide the algorithm to find the optimal set of premisses. In Chapter 5 we use the algorithm to decide formulae in a wide range of modal systems. We...
|
|
|
Automated Theorem Proving using the Tableaux method
Jakubův, Jan ; Štěpánek, Petr (vedoucí práce) ; Hric, Jan (oponent)
V této práci studujeme tableaux kalkul a podobné metody. Nejprve zavádíme obvyklé pojmy a poté představujeme tableaux kalkul pro logiku prvního řádu. Dále představujeme automatický dokazovač vět autorů Beckert a Possega [5]. Rozšiřujeme tento dokozovač o metodu, která má urychlit jeho práci. Výsledný program porovnáváme s jeho původní verzí. Dále představujeme deduktivní systém T autorů Degtyarev a Voronkov [3]. Hlavním přínosem této práce je implementace tohoto systému. Dále také vyvíjíme knihovnu pro práci s objekty logiky prvního řádu v programovacím jazyce Python.
|
|
| |
host ::
RSS.