|
Zhodnocení institutu nespolehlivého plátce při eliminaci úniků na dani z přidané hodnoty
Lišková, Svatava ; Kukalová, Gabriela (vedoucí práce) ; Jiří, Jiří (oponent)
V boji proti daňovým únikům na dani z přidané hodnoty využívá Finanční správa České republiky různé nástroje a postupy. Za jeden ze stěžejních nástrojů je považován institut nespolehlivého plátce. Předkládaná diplomová práce si klade za cíl zachytit ve všeobecné rovině základní princip fungování institutu nespolehlivého plátce, detekovat jeho nedostatky a navrhnout možná řešení zlepšení jeho využití. Hlavní důraz je přitom kladen na kritické posouzení jednotlivých charakteristik, které vedly správce daně na vybraném pracovišti k vydání rozhodnutí o nespolehlivém plátci. Závěrečná část práce z celkového pohledu zhodnocuje zavedení tohoto institutu při eliminaci daňových úniků na dani z přidané hodnoty.
|
|
Mikrobiota trávicího traktu včel a příbuzného hmyzu a faktory ovlivňující její složení
Hroncová, Zuzana ; Havlík, Jaroslav (vedoucí práce) ; Kalous, Lukáš (oponent)
Disertační práce se skládá ze šesti výzkumných kapitol, z nichž pět již bylo publikováno ve vědeckých časopisech, jeden je v oponentském řízení a poslední kapitola představuje originální nepublikovaná data v procesu přípravy rukopisu.
Výzkum prezentovaný v této práci se zabývá složitými mechanismy imunitního systému včel a vos, se zaměřením na mikrobiotu jako součást imunity. Jak je popsáno v úvodu, sociální hmyz, jako včely a čmeláci, hrají klíčovou roli v ekosystémech po celém světě. Nedávné ztráty včel jsou připisovány používání pesticidů, špatné výživě, zvýšenému infekčnímu tlaku a ničení přírodních stanovišť. Během několika posledních let se včelaři i široká veřejnost zabývají úbytky včelstev po celém světě a dožadují se dalšího výzkumu zaměřeného na řešení těchto problémů. Naším hlavním cílem bylo prozkoumat vazby střevní bakteriální populace včel a příbuzných druhů, jejich propojení s imunitou a zjistit možnosti ovlivnění těchto vztahů prostřednictvím suplementace. Součástí cíle bylo charakterizovat střevní mikrobiotu čmeláků a vos pomocí 16S RNA sekvenování, použitého při hledání potenciálně nových bakteriálních druhů.
V práci jsme se snažili objasnit, jak mikrobiom interaguje s hostitelem a prokázat, že hlavní členy těchto komunit ho pozitivně ovlivňují. Bakteriální komunity nacházející se v trávicím traktu včel, jsou ideálním modelem pro zkoumání evolučních a genetických vztahů. Informace založené na našich výsledcích můžou díky objasněným fyziologickým podmínkám v trávicím traktu včel pomoci při vývoji vhodných probiotických preparátů.
|
|
Hra jako prostředek zvyšování motivace ve vyučování odborných předmětů
Kolmanová, Linda ; Hanušová, Marie (vedoucí práce) ; Drahomíra, Drahomíra (oponent)
Bakalářská práce s názvem Hra jako prostředek zvyšování motivace ve vyučování odborných předmětů, slouží pro potřeby vhledu do problematiky motivace ve škole a jejího zvyšování prostřednictvím aktivizační metody konkrétně hry. Teoretická část přibližuje základní pojmy, které souvisí s motivy, motivací ve škole a aktivizačními metodami ve výuce, jež jsou základem pro vypracování praktické části. V praktické části je pomocí pozorování a závěrečného testu ve výukovém bloku ověřena navržená desková ekonomická hra, jakožto aktivizační metoda pro zvýšení motivace žáků ekonomického oboru. V neposlední řadě jsou představeny výsledky a provedeno zhodnocení.
|
|
Čtenářský deník a ICT - tradiční výuková metoda v kontextu moderních technologií
GRÚZ, Michael
Rigorózní práce Čtenářský deník a ICT tradiční výuková metoda v kontextu moderních technologií je rozdělena na dva oddíly. Teoretická část se nejprve zabývá základními principy uměleckého textu, jeho recepcí a motivací k četbě. Pozornost je dále věnována literární a čtenářské výchově ve škole, ale i v mimoškolním životě dítěte, a to i v tzv. předčtenářském období. Stěžejní oddíl je zaměřen na vliv moderních technologií na výuku literatury a problematiku čtenářských (kulturních) deníků. Výzkumná část obsahuje výsledky dvou dotazníkových šetření. První z nich bylo určeno pro učitele českého jazyka a literatury, kteří působí na druhém stupni základních škola a na nižším stupni gymnázií, a kladlo si za úkol zmapovat jejich přístup k zadávání, kontrole, hodnocení a dalšímu využití čtenářských deníků v hodinách literární výchovy. Druhý dotazník zjišťoval žákovský přístup k individuální mimočítankové četbě a využívání tzv. online literárních příruček.
|
|
Laserové chlazení zachycených iontů pro metrologii frekvence a času
Číp, Ondřej ; Pham, Minh Tuan ; Čížek, Martin ; Lešundák, Adam ; Hucl, Václav ; Hrabina, Jan ; Řeřucha, Šimon ; Jedlička, Petr ; Lazar, Josef
Současný výzkum v oboru laserového chlazení zachycených iontů vede k získání izolovaných iontů v základním pohybovém stavu. Detekce excitovaného Dopplerovsky zchlazeného iontu na jeho kvadrupólový přechod elektronické struktury dává příležitost ke stabilizaci vysoce koherentních laserů na optické frekvenci řádu stovek THz. Tímto způsobem lze definovat nový standard času či optické frekvence zvaný "Optické atomové hodiny". Ústav přístrojové techniky v Brně ve spolupráci s Katedrou optiky Univerzity Palackého v Olomouci realizují unikátní výzkumnou infrastrukturu pro laserové chlazení 40Ca+ iontů a následné experimenty kvantové mechaniky a spektroskopie ve společné laboratoři v Brně. V současnosti jsou rutinně generovány a zachytávány 40Ca+ ionty. Je prováděno jejich Dopplerovské chlazení prostřednictvím dipólového přechodu na vlnové délce 397 nm a prováděna detekce a spektroskopie elektronické struktury iontu a výskyt jeho temných rezonancí.
|
|
Analýza vlivu používání technických zařízení řidičem na reakční dobu
Kubánek, Ondřej ; Bradáč, Albert (oponent) ; Panáček, Vladimír (vedoucí práce)
Tato diplomová práce se zabývá analýzou vlivu používání technických zařízení řidičem na reakční dobu. Jsou zde popsány zákonné požadavky na používání technických zařízení řidičem ve vozidle. Rozebrány typy používaných technických zařízení řidiči a především probrána problematika reakční doby řidičů. Jsou posouzeny vlivy působící na reakční dobu, způsoby měření reakční doby a typy reakčních dob. Jsou rozebrány starší výzkumy z počátků měření reakčních dob až po nejnovější výzkumy, zabývající se měřením reakčních dob při používání mobilního telefonu. Praktická část práce je věnována provedení jízdních zkoušek na vybraném vzorku řidičů a vyhodnocení jejich reakčních dob při běžné jízdě a při telefonování. Naměřená a vyhodnocená data jsou okomentována s ohledem na přínos ve znalecké činnosti oboru doprava.
|
|
New Methods for Increasing Efficiency and Speed of Functional Verification
Zachariášová, Marcela ; Dohnal, Jan (oponent) ; Steininger, Andreas (oponent) ; Kotásek, Zdeněk (vedoucí práce)
In the development of current hardware systems, e.g. embedded systems or computer hardware, new ways how to increase their reliability are highly investigated. One way how to tackle the issue of reliability is to increase the efficiency and the speed of verification processes that are performed in the early phases of the design cycle. In this Ph.D. thesis, the attention is focused on the verification approach called functional verification. Several challenges and problems connected with the efficiency and the speed of functional verification are identified and reflected in the goals of the Ph.D. thesis. The first goal focuses on the reduction of the simulation runtime when verifying complex hardware systems. The reason is that the simulation of inherently parallel hardware systems is very slow in comparison to the speed of real hardware. The optimization technique is proposed that moves the verified system into the FPGA acceleration board while the rest of the verification environment runs in simulation. By this single move, the simulation overhead can be significantly reduced. The second goal deals with manually written verification environments which represent a huge bottleneck in the verification productivity. However, it is not reasonable, because almost all verification environments have the same structure as they utilize libraries of basic components from the standard verification methodologies. They are only adjusted to the system that is verified. Therefore, the second optimization technique takes the high-level specification of the system and then automatically generates a comprehensive verification environment for this system. The third goal elaborates how the completeness of the verification process can be achieved using the intelligent automation. The completeness is measured by different coverage metrics and the verification is usually ended when a satisfying level of coverage is achieved. Therefore, the third optimization technique drives generation of input stimuli in order to activate multiple coverage points in the veri\-fied system and to enhance the overall coverage rate. As the main optimization tool the genetic algorithm is used, which is adopted for the functional verification purposes and its parameters are well-tuned for this domain. It is running in the background of the verification process, it analyses the coverage and it dynamically changes constraints of the stimuli generator. Constraints are represented by the probabilities using which particular values from the input domain are selected. The fourth goal discusses the re-usability of verification stimuli for regression testing and how these stimuli can be further optimized in order to speed-up the testing. It is quite common in verification that until a satisfying level of coverage is achieved, many redundant stimuli are evaluated as they are produced by pseudo-random generators. However, when creating optimal regression suites, redundancy is not needed anymore and can be removed. At the same time, it is important to retain the same level of coverage in order to check all the key properties of the system. The fourth optimization technique is also based on the genetic algorithm, but it is not integrated into the verification process but works offline after the verification is ended. It removes the redundancy from the original suite of stimuli very fast and effectively so the resulting verification runtime of the regression suite is significantly improved.
|
|
Subspace Modeling of Prosodic Features for Speaker Verification
Kockmann, Marcel ; Kenny, Patrick (oponent) ; Nöth, Elmar (oponent) ; Černocký, Jan (vedoucí práce)
The thesis investigates into speaker verification by means of prosodic features. This includes an appropriate representation of speech by measurements of pitch, energy and duration of speech sounds. Two diverse parameterization methods are investigated: the first leads to a low-dimensional well-defined set, the second to a large-scale set of heterogeneous prosodic features. The first part of this work concentrates on the development of so called prosodic contour features. Different modeling techniques are developed and investigated, with a special focus on subspace modeling. The second part focuses on a novel subspace modeling technique for the heterogeneous large-scale prosodic features. The model is theoretically derived and experimentally evaluated on official NIST Speaker Recognition Evaluation tasks. Huge improvements over the current state-of-the-art in prosodic speaker verification were obtained. Eventually, a novel fusion method is presented to elegantly combine the two diverse prosodic systems. This technique can also be used to fuse the higher-level systems with a high-performing cepstral system, leading to further significant improvements.
|
|
Acceleration Methods for Evolutionary Design of Digital Circuits
Vašíček, Zdeněk ; Miller, Julian (oponent) ; Zelinka,, Ivan (oponent) ; Sekanina, Lukáš (vedoucí práce)
Although many examples showing the merits of evolutionary design over conventional design techniques utilized in the field of digital circuits design have been published, the evolutionary approaches are usually hardly applicable in practice due to the various so-called scalability problems. The scalability problem represents a general problem that refers to a situation in which the evolutionary algorithm is able to provide a solution to a small problem instances only. For example, the scalability of evaluation of a candidate digital circuit represents a serious issue because the time needed to evaluate a candidate solution grows exponentially with the increasing number of primary inputs. In this thesis, the scalability problem of evaluation of a candidate digital circuit is addressed. Three different approaches to overcoming this problem are proposed. Our goal is to demonstrate that the evolutionary design approach can produce interesting and human competitive solutions when the problem of scalability is reduced and thus a sufficient number of generations can be utilized. In order to increase the performance of the evolutionary design of image filters, a domain specific FPGA-based accelerator has been designed. The evolutionary design of image filters is a kind of regression problem which requires to evaluate a large number of training vectors as well as generations in order to find a satisfactory solution. By means of the proposed FPGA accelerator, very efficient nonlinear image filters have been discovered. One of the discovered implementations of an impulse noise filter consisting of four evolutionary designed filters is protected by the Czech utility model. A different approach has been introduced in the area of logic synthesis. A method combining formal verification techniques with evolutionary design that allows a significant acceleration of the fitness evaluation procedure was proposed. The proposed system can produce complex and simultaneously innovative designs, overcoming thus the major bottleneck of the evolutionary synthesis at gate level. The proposed method has been evaluated using a set of benchmark circuits and compared with conventional academia as well as commercial synthesis tools. In comparison with the conventional synthesis tools, the average improvement in terms of the number of gates provided by our system is approximately 25%. Finally, the problem of the multiple constant multiplier design, which belongs to the class of problems where a candidate solution can be perfectly evaluated in a short time, has been investigated. We have demonstrated that there exists a class of circuits that can be evaluated efficiently if a domain knowledge is utilized (in this case the linearity of components).
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis is focused on techniques for finite automata and their use in practice, with the main emphasis on nondeterministic tree automata. This concerns namely techniques for size reduction and language inclusion testing, which are two problems that are crucial for many applications of tree automata. For size reduction of tree automata, we adapt the simulation quotient technique that is well established for finite word automata. We give efficient algorithms for computing tree automata simulations and we also introduce a new type of relation that arises from a combination of tree automata downward and upward simulation and that is very well suited for quotienting. The combination principle is relevant also for word automata. We then generalise the so called antichain universality and language inclusion checking technique developed originally for finite word automata for tree automata. Subsequently, we improve the antichain technique for both word and tree automata by combining it with the simulation-based inclusion checking techniques, significantly improving efficiency of the antichain method. We then show how the developed reduction and inclusion checking methods improve the method of abstract regular tree model checking, the method that was the original motivation for starting the work on tree automata. Both the reduction and the language inclusion methods are based on relatively simple and general principles that can be further extended for other types of automata and related formalisms. An example is our adaptation of the reduction methods for alternating Büchi automata, which results in an efficient alternating automata size reduction technique.
|
host ::
