National Repository of Grey Literature 26,085 records found  beginprevious21 - 30nextend  jump to record: Search took 0.64 seconds. 

Sorption and Stabilization of Metals/Mettalloids by Innovative Synthesized Sorbent Amochar.
Ouředníček, P. ; Trakal, L. ; Komárek, M. ; Pohořelý, Michael
Remediation of contaminated soil which is based on stabilization and immobilization of potential\nhazardous substance by sorption materials has been studied intensively nowadays. Biochar – activated organic carbon belongs to this group of stabilizing agents which can adsorb wide range of contaminants, including metals/metalloids. Surface area of the biochars is quite large in general and functional groups (e.g. COO–) can form chelates or alkaline elements on the surface, which is represented by cation exchange capacity. Altogether with the high pH values (7.00 – 10.00), biochars are quite effective sorbents and can adsorb metals/metalloids from the solution (ground water), especially in acidic soils (in the environments affected by intensive mining activities). Sorption\neffectiveness can be increased (especially for As (V) or Cr (VI) sorption) by modification of biochar by various types of secondary oxides. Innovative sorbent AMOchar (AMO + biochar) has been synthesized currently. The product was prepared by adding of biochar to the reaction solution during amorphous manganese oxide (AMO) synthesis. The AMOchar was formed mainly by Mn-oxalates which had coated surface of the pristine biochar. AMOchar composite was able to remove significantly higher amounts of various metal(loid)s from the solution despite the rather high pH of the material. Sorption effectiveness was high not only in case of Pb (II) sorption (almost 99%), and Cd(II) (51.2%), but also a very high amount of As(V), 91.4%. Additionally, both AMOchar composite was able to reduce Mn leaching. This can avoid potential post-contamination caused by the dissolution of less stable Mn-oxalates as observed in the pure AMO.
Fulltext: content.csg - Download fulltextPDF
Plný tet: SKMBT_22316111113040 - Download fulltextPDF

Marketing plan
Nosálová, Lucie ; Štůsek, Jaromír (advisor) ; Ladislav , Ladislav (referee)
The goal of this thesis is to detect errors in the management of small family business, which basically does not use marketing. Following this finding should be to build an effective marketing plan. The diploma thesis is divided into theoretical part, which forms the basis for the analytical part. In the analytical part is described the company and there are also detect errors in the management that are caused by faulty marketing. To achieve results it is important to use several different types of analysis on which it is necessary to set new marketing goals, strategies, changes and projects. The aim is to provide business information and convince him that use of good marketing communication should lead to improve management efficiency and ultimatem increase profitability of the company, without the need to break away from the corporate goal of maximum efforts to build a pro-customer oriented service.

Tenancy spouses and use of the flat spouses in a new arrangement after January 1, 2014
Prantlová, Soňa ; Kadlecová, Eva (advisor) ; Pavla, Pavla (referee)
The thesis is devoted to the topic of tenancy by the spouses, and its use as is specified in the new adaptation of the Civil Code no. 89/2012 Coll. It replaced until functioning Civil Code from the year 1964. The new legislation is specified series of new institutes, whose primary aim is to protect the weaker party, in the case of tenant. The diploma thesis was divided into theoretical and practical part. In the theoretical part, was attention paid to basic concepts which have been defined. There were characterized rights of tenant and landlord, analyzed housing legislation according to the new Civil Code. The practical part was devoted to the interpretation of survey results. There were approached tenants of several apartment buildings in Kralupy nad Vltavou. Based on the findings, were designed some recommendations to raise awareness about the rights and responsibilities of tenants, as well as about the whole issue of housing legally.

Partial Report IV / 2016 - Rating of the deformation stress monitoring the state of the rock mass during mining coal seam 30 (634) within the trial operation of mining method corridor - a pillar in OPJ ČSM - NORTH
Waclawik, Petr ; Ptáček, Jiří ; Kukutsch, Radovan ; Kajzar, Vlastimil ; Koníček, Petr ; Souček, Kamil ; Staš, Lubomír
Monitoring of the deformation stress state of the rock mass is a prerequisite for the verification of unapproved new mining methods hall-pillar and its further application in the Czech part of the Upper Silesian coal basin. This mining method is designed on the basis of experiences and practices that are verified in different natural conditions and depths below the surface and is therefore essential for the verification of conditions for the Czech part of the Upper Silesian Basin based on geotechnical monitoring. The present report is prepared on the basis of a contract no. 942/50/10, where the Institute of Geonics, v.v agrees to make periodic evaluation of monitoring data napěťodeformačního state of the rock mass. In accordance with the aforementioned agreement, the message is processed in the six-month period and continues in the interim report III / 2015 (Waclawik et al. 2015) passed buyers in April this year. Interim results of the geotechnical monitoring, such as the experience gained during the first conquest dobývky V show specifics of natural conditions in trial operation unapproved new mining methods hall-pillar.
Fulltext: content.csg - Download fulltextPDF
Plný tet: UGN_0464907 - Download fulltextPDF

Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.

Analysis and Testing of Concurrent Programs
Letko, Zdeněk ; Lourenco, Joao (referee) ; Sekanina, Lukáš (referee) ; Vojnar, Tomáš (advisor)
V disertační práci je nejprve uvedena taxonomie chyb v souběžném zpracování dat a přehled technik pro jejich dynamickou detekci. Následně jsou navrženy nové metriky pro měření synchronizace a souběžného chování programů společně s metodologií jejich odvozování. Tyto techniky se zejména uplatní v testování využívajícím techniky prohledávání prostoru a v saturačním testování. Práce dále představuje novou heuristiku vkládání šumu, jejímž cílem je maximalizace proložení instrukcí pozorovaných během testování. Tato heuristika je porovnána s již existujícími heuristikami na několika testech. Výsledky ukazují, že nová heuristika překonává ty existující v určitých případech. Nakonec práce představuje inovativní aplikaci stochastických optimalizačních algoritmů v procesu testování vícevláknových aplikací. Principem metody je hledání vhodných kombinací parametrů testů a metod vkládání šumu. Tato metoda byla prototypově implementována a otestována na množině testovacích příkladů. Výsledky ukazují, že metoda má potenciál vyznamně vylepšit testování vícevláknových programů. 

Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Tato práce představuje nové metody pro verifikaci programů pracujících s neomezenými celočíslenými proměnnými, konkrétně metody pro analýzu dosažitelnosti a~konečnosti. Většina těchto metod je založena na akceleračních technikách, které počítají tranzitivní uzávěry cyklů programu. V práci je nejprve představen algoritmus pro akceleraci několika tříd celočíselných relací. Tento algoritmus je až o čtyři řády rychlejší než existující techniky. Z teoretického hlediska práce dokazuje, že uvažované třídy relací jsou periodické a~poskytuje tudíž jednotné řešení prolému akcelerace. Práce dále představuje semi-algoritmus pro analýzu dosažitelnosti celočíselných programů, který sleduje relace mezi proměnnými programu a~aplikuje akcelerační techniky za účelem modulárního výpočtu souhrnů procedur. Dále je v práci navržen alternativní algoritmus pro analýzu dosažitelnosti, který integruje predikátovou abstrakci s accelerací s cílem zvýšit pravděpodobnost konvergence výpočtu. Provedené experimenty ukazují, že oba algoritmy lze úspěšně aplikovat k verifikaci programů, na kterých předchozí metody selhávaly. Práce se rovněž zabývá problémem konečnosti běhu programů a~dokazuje, že tento problém je rozhodnutelný pro několik tříd celočíselných relací. Pro některé z těchto tříd relací je v práci navržen algoritmus, který v polynomiálním čase vypočítá množinu všech konfigurací programu, z nichž existuje nekonečný běh. Tento algoritmus je integrován do metody, která analyzuje konečnost běhů celočíselných programů. Efektivnost této metody je demonstrována na několika netriviálních celočíselných programech.

Grammars with Restricted Derivation Trees
Koutný, Jiří ; Janoušek, Jan (referee) ; Vojnar, Tomáš (referee) ; Meduna, Alexandr (advisor)
V této disertační práci jsou studovány teoretické vlastnosti gramatik s omezenými derivačními stromy. Po uvedení současného stavu poznání v této oblasti je výzkum zaměřen na tři základní typy omezení derivačních stromů. Nejprve je představeno zcela nové téma, které je založeno na omezení řezů a je zkoumána vyjadřovací síla takto omezené gramatiky. Poté je zkoumáno několik nových vlastností omezení kladeného na cestu derivačních stromů. Zejména je studován vliv vymazávacích pravidel na vyjadřovací sílu gramatik s omezenou cestou a pro tyto gramatiky jsou zavedeny dvě normální formy. Následně je popsána nová souvislost mezi gramatikami s omezenou cestou a některými pseudouzly. Dále je prezentován protiargument k vyjadřovací síle tohoto modelu, která byla dosud považována za dobře známou vlastnost. Nakonec je zavedeno zobecnění modelu s omezenou cestou na ne jednu, ale několik cest. Tento model je následně studován zejména z hlediska vlastností vkládání, uzávěrových vlastností a vlastností syntaktické analýzy.

Evolutionary Approach to Synthesis and Optimization of Ordinary and Polymorphic Circuits
Gajda, Zbyšek ; Schmidt, Jan (referee) ; Zelinka,, Ivan (referee) ; Sekanina, Lukáš (advisor)
Tato disertační práce se zabývá evolučním návrhem a optimalizací jak běžných, tak polymorfních digitálních obvodů. V práci jsou uvedena a vyhodnocena nová rozšíření kartézského genetického programování (Cartesian Genetic Programming, CGP), která umožňují zkrácení výpočetního času a získávání kompaktnějších obvodů. Další část práce se zaměřuje na nové metody syntézy polymorfních obvodů. Uvedené metody založené na polymorfních binárních rozhodovacích diagramech a polymorfním multiplexovaní rozšiřují běžné reprezentace digitálních obvodů, a to s ohledem na začlenění polymorfních hradel. Z důvodu snížení počtu hradel v obvodech syntetizovaných uvedenými metodami je provedena evoluční optimalizace založená na CGP. Implementované polymorfní obvody, které jsou optimalizovány s využitím CGP, reprezentují nejlepší známá řešení, jestliže je jako cílové kritérium brán počet hradel obvodu.

Synchronous Formal Systems Based on Grammars and Transducers
Horáček, Petr ; Janoušek, Jan (referee) ; Yamamura,, Akihito (referee) ; Meduna, Alexandr (advisor)
Tato disertační práce studuje synchronní formální systémy založené na gramatikách a převodnících a zkoumá jak jejich teoretické vlastnosti, tak i perspektivy praktických aplikací. Práce představuje nové koncepty a definice vycházející ze známých principů řízeného přepisování a synchronizace. Navrhuje alternativní způsob synchronizace bezkontextových gramatik, založený na propojení pravidel. Tento princip rozšiřuje také na řízené gramatiky, konkrétně gramatiky s rozptýleným kontextem a maticové gramatiky. Dále je představen na podobném principu založený nový druh převodníku, tzv. pravidlově omezený převodník. Jedná se o systém složený z konečného automatu a bezkontextové gramatiky. Práce prezentuje nové teoretické výsledky ohledně generativní a přijímajicí síly. Poslední část práce zkoumá možnosti lingvisticky orientovaných aplikací se zameřením na překlad přirozeného jazyka. Diskutuje a srovnává hlavní výhody nových modelů s využitím vybraných případových studií z českého, anglického a japonského jazyka pro ilustraci.