|
Význam Rady bezpečnosti OSN a právní závaznost rezolucí při zajišťování mezinárodního míru a bezpečnosti
Urbanová, Petra ; Ondřej, Jan (vedoucí práce) ; Balaš, Vladimír (oponent)
- Význam Rady bezpečnosti OSN a právní závaznost rezolucí při zajišťování mezinárodního míru a bezpečnosti Tato práce pojednává o historii předcházející vzniku, a o samotném vzniku OSN a Rady bezpečnosti, na který navazuje kapitola věnující se stálým a nestálým členům Rady s podkapitolou týkající se reformních návrhů z hlediska jejího složení. Podrobně jsou zde rozebrány funkce a pravomoci Rady bezpečnosti, obsahující také pasáž týkající se období ochromení činnosti Rady. V kapitole o způsobu usnášení Rady je věnována pozornost jak zásadní problematice rozlišení otázek procedurálních a neprocedurálních, tak institutu veta. Závěrečná kapitola se věnuje rozhodnutím Rady bezpečnosti se zaměřením na rezoluce a jejich právní závaznost.
|
|
Proces s Miladou Horákovou v kontextu dobové propagandy
Srb, Petr ; Jančík, Drahomír (vedoucí práce) ; Jakubec, Ivan (oponent)
Práce je analýzou dobových propagandistických metod vládnoucí moci a jejich působení na české a slovenské obyvatelstvo. Je zasazena do širšího dobového kontextu. Středem pozornosti jsou rezoluce a jejich analýza, je zohledněna dobová publicistika a je učiněn pokus o detailnější komparaci procentuálního zastoupení tematicky zaměřených článků na stránkách dvou vybraných deníků. Práce je založena především na archivním materiálu vztahujícímu se k procesu s Miladou Horákovou, který se nachází v Národním archivu v Praze, dále pak vychází z dobové publicistiky a navazuje na soudobou odbornou historickou literaturu. Klíčová slova: Milada Horáková, politické procesy, rezoluce
|
|
Hledání minimálních splňujících ohodnocení Booleovských formulí
Švancara, Jiří ; Balyo, Tomáš (vedoucí práce) ; Trunda, Otakar (oponent)
V této práci zkoumáme algoritmy a techniky pro řešení Booleovské splnitelnosti. Dále se zabýváme možnostmi jejich použití při řešení weighted short SAT, což je zobecnění problému splnitelnosti. Toto zobecnění požaduje nalézt splňující ohodnocení za použití minimálního součtu vah proměnných. K řešení tohoto problému zavádíme tři pravdivostní ohodnocení proměnných - True, False a Unassign. Ukážeme, že ne všechny algoritmy a techniky používané v moderních SAT solverech můžeme aplikovat v našem programu. Ty, které můžeme, převedeme tak, aby používali námi nadefinované pravdivostní ohodnocení. Různou kombinací takto převedených technik dostaneme několik verzí solveru, které mezi sebou na závěr porovnáme. Powered by TCPDF (www.tcpdf.org)
|
|
On the Power of Weak Extensions of V0
Müller, Sebastian Peter ; Krajíček, Jan (vedoucí práce) ; Thapen, Neil (oponent) ; Kolodziejczyk, Leszek (oponent)
Název práce: O síle slabých rozšírení teorie V0 Autor: Sebastian Müller Katedra: Katedra Algebry Vedoucí disertační práce: Prof. RNDr. Jan Krajíček, DrSc., Katedra Algebry. Abstrakt: V predložené disertacní práci zkoumáme sílu slabých fragmentu arit- metiky. Činíme tak jak z modelově-teoretického pohledu, tak z pohledu důkazové složitosti. Pohled skrze teorii modelu naznačuje, že malý iniciální segment libo- volného modelu omezené aritmetiky bude modelem silnější teorie. Jako příklad ukážeme, že každý polylogaritmický řez modelu V0 je modelem VNC. Užitím známé souvislosti mezi fragmenty omezené aritmetiky a dokazatelností v ro- zličných důkazových systémech dokážeme separaci mezi rezolucí a TC0 -Frege systémem na náhodných 3CNF-formulích s jistým poměrem počtu klauzulí vůci počtu proměnných. Zkombinováním obou výsledků dostaneme slabší separační výsledek pro rezoluci a Fregeho důkazové systémy omezené hloubky. Klíčová slova: omezená aritmetika, důkazová složitost, Fregeho důkazový systém, Fregeho důkazový systém omezené hloubky, rezoluce Title: On the Power of Weak Extensions of V0 Author: Sebastian Müller Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., Department of Algebra....
|
|
Implementace mandátu mise UNPROFOR v Bosně a Hercegovině v letech 1992-1995
Lalić, Jan ; Tejchman, Miroslav (vedoucí práce) ; Pikal, Kamil (oponent)
Neochota mezinárodního společenství zapojit se do bosenské občanské války v letech 1992- 1995 vojenskou intervencí, vytvořila z mise United Nations Protection Force (UNPROFOR) náhražku rozhodné akce. Absence jakékoliv naděje na dohledné příměří, které by mohly mírové jednotky svojí přítomností podporovat, vedla v první fázi války k vytvoření ryze humanitárního mandátu pro jednotky OSN. Ty měly ve spolupráci s Úřadem vysokého komisaře OSN pro uprchlíky (UNHCR) zajistit chod sarajevského letiště pro humanitární účely a postarat se o bezpečnost UNHCR a jeho konvojů s humanitární pomocí. Práce "Implementace mandátu mise UNPROFOR v Bosně a Hercegovině v letech 1992-1995" se zabývá právě problematikou implementace tohoto čistě humanitárního mandátu. Pomocí deskriptivní analýzy nejdříve vysvětlí motivy, které vedly mezinárodní společenství k nasazení lehce vyzbrojených mírových jednotek s netypickým mandátem do oblasti, která se ukáže být naprosto nevhodnou pro působení mírových sil. Následně prozkoumá samotný průběh implementace a problémy, se kterými se jednotky OSN potýkaly. Cílem práce je dokázat, že mise UNPROFOR nebyla absolutním selháním, za jaké je pokládána, avšak prokáže se neadekvátnost jejího nasazení v daném prostředí a budou představeny příčiny neúspěchů.
|
|
Metody odhadů složitosti důkazů ve výrokové logice
Peterová, Alena ; Pudlák, Pavel (vedoucí práce) ; Krajíček, Jan (oponent)
V této práci se věnujeme složitosti důkazových systémů pro výrokovou logiku. Nejprve ukážeme exponenciální dolní odhad na složitost rezoluce přímou aplikací Razborovovy aproximační metody, která byla dosud používána pouze pro odhady na velikost monotónních obvodů. Následně použijeme aproximační metodu i pro nový důkaz exponenciálního dolního odhadu na složitost náhodných rezolučních důkazů. To by mělo mít další využití při separování různých teorií v omezené aritmetice. V obou případech využijeme problém z teorie grafů zvaný Broken Mosquito Screens. Na závěr vyslovíme hypotézu, že aproximační metoda bude mít využití i v silnějších důkazových systémech, jako například Cutting Planes. Powered by TCPDF (www.tcpdf.org)
|