|
|
Simulation of transactions on Stock Market
Ulrych, Stanislav ; Jakob, Michal (referee) ; Štěpánek, Petr (advisor)
This diploma thesis presents the simulation of the high frequency trading (HFT) strategies on electronic markets such as NASDAQ. The simulation is based on merging real historical order flow data and order flow of artificial trading agents representing new HFT strategies. This concept has not yet been widely discussed elsewhere. The problems discussed include: processing order flow market data, very precise time referencing, parametric reaction latency, various order types distinction etc. The design and the implementation of simulation process are presented, with respect to high computational requirements, modularizable strategies implementation and parallelization of whole simulation. In the final part of the work, we discuss the implementation and the results of a simulation of a simple HFT strategy.
|
|
|
Koordinace mezi logickými agenty
Krištofič, Milutín ; Vojtáš, Peter (referee) ; Štěpánek, Petr (advisor)
In this thesis, we study the recent models for coordination and we propose a new model based on argumentation system. This system, named Argumentation BlackBoard for Coordination (ABBC), and its extension, Abstract ABBC, are based on successful argumentation approaches, such as abstract argumentation framework and defeasible logic programming. Our aim is to present necessary argumentation elements in open multi-agent system that consists of logic agents. In this work, we also describe a brief software design for the system.
|
|
|
Systems for formal mathematics
Kunčar, Ondřej ; Štěpánek, Petr (referee) ; Urban, Josef (advisor)
The Mizar type system is a relatively sophisticated system as it allows for many properties, such as independent types, attributes, overloading, subtyping, structures and many others. All these properties make formalization of mathematics more intuitive in Mizar that in other systems. However, there is a need to verify mathematical results formalized in Mizar in other systems, so that belief in consistency of Mizar system is strengthened. Attempts at reconstruction of this type system in other mathematics formalization systems follow directly from this requisite. The present work seeks to reconstruct Mizar type system in HOL Light system. The basic idea here is to represent Mizar types as predicates in this system (HOL Light). The present work also aims at precise description of relevant parts of Mizar type system. The thesis concludes by reviewing some of the insights that were arrived at in the course of designing and implementing suggested reconstruction.
|
|
|
Metaphors and Modelling of Life Systems
Ibrahimová, Nora ; Štěpánek, Petr (referee) ; Havel, Ivan (advisor)
The aim of this work is to theoretically study and describe some of the models of living systems. In the rst part, we focus on models of autonomous systems, such as the cell or a living being as a whole. In this part, we introduce the principle of autopoiesis and a mathematical model of an autopoietic system. We also analyse other related and philosophically relevant terms and principles. In the second part, we describe in detail and compare two dynamic models of brain. Both parts take the so-called enactive approach, and use the terms and principles of the dynamic systems theory. As a part of this work, a model of one of the key terms - sensorimotor skills - has been created using neural networks.
|
|
| |
|
|
eHealth: new media in health service
Bartůňková, Lucie ; Štěpánek, Petr (advisor) ; Šlerka, Josef (referee)
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.
|
|
|
Media education in the Czech Republic focused on the new media
Marková, Anna ; Štěpánek, Petr (advisor) ; Štogr, Jakub (referee)
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 (advisor) ; Haniková, Zuzana (referee) ; Plátek, Martin (referee)
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 (advisor) ; Hric, Jan (referee)
In this paper we are studying the Tableaux Calculus a related methods. We adopt basic notions and present the tableaux calculus for the First-Order Logic. Then we present the Beckert and Possega [5] prover. We extend this prover with speed-up technique and compare the results with the original prover. Then we present the tableaux T system of Degtyarev and Voronkov [3] supposed to handle the equality. The main benefit of this paper is the implementation the the T system prover. We also present a library providing tools to work with the objects of the First-Order Logic in the programming language Python.
|
|
| |
guest ::
RSS feed.