Národní úložiště šedé literatury Nalezeno 32 záznamů.  1 - 10dalšíkonec  přejít na záznam: Hledání trvalo 0.00 vteřin. 
(Im)possibilty results in Proof Complexity and Arithmetic
Khaniki, Erfan ; Pudlák, Pavel (vedoucí práce) ; Buss, Samuel (oponent) ; Kolodziejczyk, Leszek (oponent)
Názov práce: Výsledky o (ne)možnostech v důkazové složitosti a aritmetice Autor: Erfan Khaniki Katedra: Katedra Algebry Vedúci dizertačnej práce: Prof. RNDr. Pavel Pudlák, DrSc Abstrakt: Zabýváme se problémy v důkazové složitosti, omezené aritmetice a intu- icionistické aritmetice. Soustředíme se na témata jako dolní odhady pro různé důkazové systémy, souvislosti mezi generátory v důkazové složitosti a modely ar- itmetiky, operátory skoku v důkazové složitosti a nelokalitou určitých Kripkeho modelů v Heytingově aritmetice. Klíčová slova: důkazová složitost, dolní odhady, omezenená aritmetika, nezávislost, Heytin- gova aritmetika, Kripkeho modely 1
Proof Systems: A Study on Form and Complexity
Jalali Keshavarz, Raheleh ; Pudlák, Pavel (vedoucí práce) ; Metcalfe, George (oponent) ; Ramanayake, Revantha (oponent)
Důkazové systémy: forma a složitost Tato disertační práce obsahuje tři části. První dvě části spolu souvisí. V [1] a [2], Iemhoff objevila souvislost mezi existencí terminujícího sekvenčního kalkulu určitého druhu a uniformní interpolační vlastností superintuicioni- stické logiky, kterou tento kalkulus zachycuje. Ve druhé části budeme tento vztah zobecňovat tak, aby pokrýval také substrukturální nastavení na jedné straně a silnější typ systémů nazývaných semi-analytické kalkuly na straně druhé. Abychom byli přesnější, ukážeme, že jakákoli dostatečně silná sub- strukturální logika se semi-analytickým kalkulem má Craigovu interpolační vlastnost a v případě, že je kalkulus terminující, má uniformní interpo- laci. Tento vztah pak vede k některým konkrétním aplikacím. Pozitivním výsledkem je, že poskytuje jednotnou metodu k prokázání uniformní in- terpolační vlastnosti pro logiky FLe, FLew, CFLe, CFLew, IPC, CPC a některá z jejich modálních rozšíření K a KD. Další aplikací je nega- tivní výsledek, že mnohé substrukturální logiky, včetně Ln, Gn, BL, R a RMe , téměř všechny superintuicionistické logiky (kromě nejvýše sedmi z nich) a téměř všechna rozšíření S4 (kromě třiceti sedmi z nich)...
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.
NP vyhledávací problémy a redukce mezi nimi
Ševčíková, Renáta ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
NP vyhledávací problémy a redukce mezi nimi Renáta Ševčíková V předložené práci studujeme třídu Total NP vyhledávacích problémů. Větší pozornost je věnována studiu podtříd této třídy a redukcí mezi nimi. Kombinujeme známé metody: vyhledávací stromy a jejich vztah k redukcím, důkaz sporem pomocí Nullstellensatz důkazového systému a dolní odhad na stupeň tohoto důkazu pomocí designů, abychom ukázali, že dvě třídy relativi- zovaných NP vyhledávacích problémů založených na Mod-p počítacím principu a Mod-q počítacím principu, kde p a q jsou různá prvočísla, nejsou mezi sebou redukovatelné. Práce je ukončena novým výsledkem separace pro p = 2 a q = 3.
Těžké tautologie
Pich, Ján ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
Skoumáme nedokazatelnost tvrzení NP$\not\subseteq$P/poly v různých fragmentech aritmetiky. Ta se obvykle dosahuje ukázáním těžkosti výrokových formulí kódujících superpolynomiální spodní odhady pro booleovské obvody. Nejprve prezentujeme několik známých technik a tvrzení. Přirozené důkazy, efektívní interpolaci, KPT větu, iterovatelnost, gadget generátory atd. Pak dokážem několik původních výsledků. Ukážeme nedokazatelnost superpolynomiálních spodních odhadů na booleovské obvody v systémech s efektívní interpolaci (modulo složitostní předpoklad) a v systémech podobajících se stromovým Frege systémům manipulujícím s formulemi, které obsahují jen málo proměnných dokazovaného tvrzení. Tyto výsledky jsou založeny na dokazování těžkosti Nisan-Wigdersonových generátorů v príslušných důkazových systémech.
In the Light of Intuitionism: Two Investigations in Proof Theory
Akbartabatabai, Seyedamirhossein ; Pudlák, Pavel (vedoucí práce) ; Beckmann, Arnold (oponent) ; Iemhoff, Rosalie (oponent)
Vo svetle intuicionizmu: dve štúdie v teórii dôkazov Táto práca pojednáva o dvoch špecifických aspektoch vzt'ahu medzi klasickou a intuicionistickou teóriou dôkazov. V prvej časti zavedieme, s použitím odvodení v klasickej aritmetike, formalizáciu pre Gödelov neformálny výklad BHK interpretácie. Gödelova interpretácia dokazatel'nosti pre intuicionistic- kú výrokovú logiku bola prvý raz publikovaná v [1]. Definoval tu modálny systém S4 ako formalizáciu pre intuitívny koncept dokazatel'nosti, a po- tom preložil IPC na S4 pri zachovaní korektnosti a úplnosti. Gödelova práca navrhuje hl'adat' interpretáciu dokazatel'nosti pre modálnu logiku S4 s použitím aritmetických dôkazov, ktorá samotná vedie k takejto interpretácii dokazatel'nosti pre intuicionistickú logiku. V prvej kapitole sa pokúsime vyriešit' tento problém. Zovšeobecníme Solovayovu interpretáciu dokazatel'- nosti pre modálnu logiku GL, aby sme zachytili iné modálne logiky, konkrétne K4, KD4 a S4. S použitím už spomínaného Gödelovho prekladu navrhneme formalizáciu BHK interpretácie pomocou dôkazov v klasickej logike. Ako dôsledok ukážeme, že BHK interpretácia je dostatočne silná a umožňuje viacero rôznych formalizácií, ktoré prekvapivo zachytávajú rôzne výrokové logiky...
NP vyhledávací problémy
Jirotka, Tomáš ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
Název práce: NP vyhledávací problémy Autor: Tomáš Jirotka Katedra: Katedra algebry Vedoucí diplomové práce: Prof. RNDr. Jan Krajíček, DrSc. Abstrakt: Práce shrnuje dosavadní výsledky v oblasti NP vyhledávacích problémů. Podrobně diskutujeme otázku složitosti faktorizace celých čísel a před- kládáme výsledky, které zařazují tento problém do již známých složitostních tříd a v jistém smyslu se jej snaží separovat z PLS. Dále definujeme několik nových vyhledávacích problémů. Klíčová slova: Výpočetní složitost, TFNP, faktorizace čísel.

Národní úložiště šedé literatury : Nalezeno 32 záznamů.   1 - 10dalšíkonec  přejít na záznam:
Viz též: podobná jména autorů
2 Pudlák, Petr
Chcete být upozorněni, pokud se objeví nové záznamy odpovídající tomuto dotazu?
Přihlásit se k odběru RSS.