|
|
Proof Complexity of CSP
Gaysin, Azza ; Krajíček, Jan (vedoucí práce) ; Kolokolova, Antonina (oponent) ; Kompatscher, Michael (oponent)
V této práce formalizujeme Zhukův polynomiální algoritmus rozhodující řešitelnost problémů splňování podmínek (CSPs), které nejsou NP-úplné, ve slabé teorii omezené aritmetiky W1 1 . Jako důsledek odvodíme, že tautologie odpovídající negativním instancím oněch CSP mají polynomiální důkazy v kvantifikovaném výrokovém počtu G. 1
|
|
|
Spectrum problem
Krejčí, Markéta ; Krajíček, Jan (vedoucí práce) ; Kompatscher, Michael (oponent)
V této práci prezentujeme pojem spektra sentence logiky prvního řádu včetně nekolika vět spojujících ho s teorií složitosti a dvou známých otevřených problémů Scholze a Assera. Ukážeme, že jsou některé zajimavé podmnožiny N+ , které tvoří spektrum - buď přímou kontrukcí nebo za použití pokročilejších vět. Nakonec dokážeme, že spektra jsou uzavřená na sjednocení, průnik, sčítání a násobení. 1
|
|
|
Monadic NP sets
Putzer, Martin ; Krajíček, Jan (vedoucí práce) ; Honzík, Radek (oponent)
Jako zobecněná spektra se označují třídy konečně axiomatisovatelné v existenční druhořádové logice s relací platnosti omezenou na konečné struktury. Jest známým faktem, že korrespondují dle Faginovy věty s prvky složitostní třídy NP. Prob- lém uzavřenosti NP na komplementaci se tedy redukuje na problém uzavřenosti zobecněných spekter na komplementaci. Důkaz P ̸= NP, za předpokladu, že ono tvrzení skutečně platí, by tak mohl spočívat v nalezení konkretního zobecněného spektra (a tedy třídy v NP), jehož doplněk, jsa arci v coNP, by nebyl prvkem NP. Hledání takového důkazu ovšem též nepřineslo úspěch. Částečné rozřešení tohoto problému (an sám je toliko speciálním příkladem obecnějšího tak zvaného prob- lému Asserova) přinesla Fagin-Hájkova věta, tvrdící, že jistá podtřída NP, třída tak zvaných monadických NP množin vskutku netvoří třídu uzavřenou na kom- plementaci. Reprodukce Faginova původního důkazu této věty, spolu s uvedením veškerého potřebného apparátu, je cílem této práce. 1
|
|
|
The incompleteness theorems and Berry's paradox
Grego, Maroš ; Krajíček, Jan (vedoucí práce) ; Kompatscher, Michael (oponent)
Tahle práce je věnovaná formální prezentaci alternativního důkazu Gödelovy první věty o neúplnosti, založeném na Berryho paradoxu ("nejmeší číslo, které nelze defino- vat méně než 57 znaky", přičemž tahle definice má méně znaků a definuje tohle číslo). Použitý přístup byl navržen v článku G. Chaitina. Definujeme Kolmogorovovu složitost přirozeného čísla m jako binární délku nejmešího programu pro univerzální Turingův stroj, který na vstupu 0 vrátí číslo m. Pomocí formálního argumentu inspirovaného Berryho paradoxem ukážeme nedokazatelnost tvrzení, že číslo n je dolní mezí pro Kol- mogorovovu složitost čísla m v jakémkoliv konzistentím rekurzivně axiomatizovatelném rozšíření Robinsonovy aritmetiky. Jednoduchý početní argument ale ukáže, že pro všechna n je tohle tvrzení pravdivé pro všechna až na konečně mnoho m. To je využito k důkazu první věty o neúplnosti. Jiný způsob (pocházející od G. S. Boolose) formalizace Berryho paradoxu k důkazu stejné věty je představen v kontextu prezentovaného přístupu. 1
|
|
|
Models of bounded arithmetic
Narusevych, Mykyta ; Krajíček, Jan (vedoucí práce) ; Šaroch, Jan (oponent)
Práce zkoumá vzájemné vztahy různých verzí zásuvkového principu (tež princip hol- ubníku) nad teorií omezené aritmetiky T1 2 (R). Základní dvě varianty jsou obyčejný PHPn+1 n (R), formalizující že R není grafem injektivní funkce z [n + 1] do [n], a jeho slabší verze, WPHP2m m (S), formalizující že S není grafem injektivní funkce z [2m] do [m]. Je známo, že teorie T1 2 (R) nedokazuje PHPn+1 n (R). Práce zobecňuje známe metody a ukazuje, že teorie T1 2 (R) plus ∀mWPHP2m m (□p 1(R)) nedokazuje PHPn+1 n (R) (kde □p 1(R) označuje relace polynomiálně definovatelné z R). Plyne to z jíž známých faktů, náš důkaz je ale elementárnější a umožňuje nám dokázat částečný výsledek směrem k otevřenému problému, který zmínil M. Ajtai (1990). 1
|
|
|
Pseudofinite structures and limits
Ježil, Ondřej ; Krajíček, Jan (vedoucí práce) ; Šaroch, Jan (oponent)
Pro třídu instancí výpočetního problému definujeme limitní objekt, vzhledem k nějaké výpočetně omezené třídě funkcí. Klíčová metoda zde je forcing s náhodnými proměnnými, kde za množinu elementárních jevů bereme instance nestandardní velikosti. Studujeme obecnou teorii těchto limit, v práci nazývaných široké limity, a jejich spojitost s klasickými problémy jako je nalezení velké kliky a nebo s kombinatorickými problémy přidruženými k třídám NP vyhledávacích problémů PPA a PPAD. Nášimi hlavními výsledky jsou určité 0-1 zákony pro tyto limity a existence kliky významné velikosti v široké limitě grafů sestávajících z jedné velké kliky. 1
|
|
|
Formování regionu a proměna jeho rolí v průběhu 20. století: Českomoravská vrchovina
Krajíček, Jan ; Klusáková, Luďa (vedoucí práce) ; Janáč, Jiří (oponent)
Region je v současnosti jedním z nejfrekventovanějších pojmů společenskovědního diskurzu. V pojetí historické vědy přitom jde o teoretický a metodologický koncept, který má již z podstaty svého časoprostorového významu výrazný mezioborový přesah, zejména v kulturní geografii a sociologii. Tato práce se zabývá možnostmi jeho využití v historickém bádání aplikovaném na konkrétní příklad regionu Českomoravské vrchoviny. Práce mapuje dosavadní stav bádání a vývoj přístupů k regionu. Nejdůležitější koncepty, které lze v případě Českomoravské vrchoviny uplatnit, jsou potom podrobně představeny. Českomoravská vrchovina byla zvolena pro svou specifickou roli zaostalé vnitřní periferie, která v průběhu 20. století zformovala do podoby centralizovaného a institucionalizovaného moderního regionu, kraje Vysočina. Základním východiskem je přitom teorie Anssiho Paasiho o formování moderních regionů. Podle ní region během procesu svého utváření k institucionalizovanému a ohraničenému prostoru nenabývá jen fyzického tvaru, ale vyvíjí se také v dimenzi symbolické, vytváří se jeho identita. V neposlední řadě má region též proměnlivou sociální a ekonomickou charakteristiku. Vlivem tohoto formování se pak během 20. století proměňuje způsob, jakým je region vnímán - proměňuje se jeho role. Práce tak sleduje nejen...
|
|
|
Analýza pigmentů z integumentu Graphosoma semipunctatum.
Krajíček, Jan ; Bosáková, Zuzana (vedoucí práce) ; Svobodová, Eva (oponent)
Pteriny patří do důležité skupiny látek, fungující jako pigmenty u řady druhů živočichů. Některé z nich jsou pravděpodobně zodpovědné za charakteristické zbarvení skupiny hmyzu. Toto zbarvení funguje jako varovný signál pro vizuálně se orientující predátory (ptáky, ještěrky aj.). Tato práce byla zaměřena na vývoj HPLC separační metody pro analýzu pterinů, obsažených v Graphosoma semipunctatum. Pro vývoj metody byl zvolen reverzní separační mód s C18 stacionární fází (Spherisorb ODS 2) a binární mobilní fází (organický modifikátor/fosfátový pufr nebo voda). V rámci optimalizační procedury byl sledován vliv typu a obsahu organického modifikátoru (methanol, ethanol, tetrahydrofuran) a koncentrace fosfátového pufru, pH 3,0 (10 - 30 mM) v mobilní fázi na retenční a separační chování studovaných pterinů (leukopterin, biopterin, xanthopterin, isoxanthopterin a erythropterin). Za optimalizovaných separačních podmínek (5/95 (v/v) methanol/20 mM fosfátový pufr, pH 3,0, průtoková rychlost 0,7 ml.min-1 , UV detekce při 290 nm) byl analyzován extrakt z integumentu ploštice Graphosoma semipunctatum.
|
|
|
Silné důkazové systémy
Mikle-Barát, Ondrej ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
R-OBDD je nový Cook-Reckhowův důkazový systém pro výrokovou logiku založen na kombinaci OBDD důkazového systému a rezolučního důkazového systému. R-OBDD má sílu OBDD důkazového systému - tautologie s exponenciálně velkými důkazy v rezoluci jako PHPn nebo Tseitinovy kontradikce mají v R-OBDD systému polynomiální důkazy (R-OBDD p-simuluje jak OBDD důkazový systém, tak rezoluci). Na druhé straně, odvozovací pravidla R-OBDD systému byly navrhnuty, aby se podobaly odvozovacím pravidlům rezoluce. Tím pádem je možné vytvořit modifikaci DPLL algoritmu, která bude pracovat v R-OBDD systému a zároveň použít některé heuristiky známé z algoritmů založených na DPLL. Vzniká možnost vytvořit efektivnejší algoritmus na řešení problému splnitelnosti formule (SAT). Ukážeme návrh algoritmu, který je adaptací DPLL algoritmu pro R-OBDD důkazový systém. Přikldáme důkaz z jeho korektnosti a ukážeme, že jeho běh nad nesplnitelnou formulí je možné transformovat do stromového důkazu v R-OBDD systému.
|
|
|
Tvorba spektrogramů a jejich zpětná syntéza
Krajíček, Jan ; Bálek, Martin (vedoucí práce) ; Pangrác, Ondřej (oponent)
V práci je popsána tvorba grafů čas-frekvence-intenzita (spektrogramů) ze zvukových nahrávek pomocí Fourierovy transformace. Dále jsou zhodnoceny teoretické možnosti a omezení zpětné syntézy zvuku ze spektrogramu a popsány dvě praktické metody syntézy, založené na rekonstrukci z čistých tónů a z náhodného šumu. Tvorba spektrogramů a obě popsané metody syntézy jsou implementovány v podobě programu s grafickým uživatelským rozhraním, které umožňuje pohodlné nastavení příslušných parametrů.
|
host ::
RSS.