|
|
(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
|
|
|
Model constructions for bounded arithmetic
Garlík, Michal ; Krajíček, Jan (vedoucí práce) ; Buss, Samuel (oponent) ; Thapen, Neil (oponent)
Název práce: Konstrukce modelů omezené aritmetiky Autor: Michal Garlík Abstrakt: Studujeme konstrukce modelů teorií omezené aritmetiky. Pomocí základních technik teorie modelů podáme nový důkaz Ajtaiovy věty o úplnosti pro nestandardně konečné struktury. Za použití omezené redukované mocniny (zobecnění ultraproduktu) navrhneme dvě nové metody konstrukce modelů ome- zené aritmetiky. První dá nový důkaz Bussovy dosvědčující věty. Druhou metodou ukážeme, že teorie R1 2 je silnější než její varianta strictR1 2 za věrohodného výpo- četně-složitostního předpokladu (existence dostatečně silné jednosměrné permu- tace) a že za stejného předpokladu je teorie PV1 + Σb 1(PV ) − LLIND silnější než PV1 + strictΣb 1(PV ) − LLIND. Pro relativizované teorie dokážeme, že R1 2(α) je silnější strictR1 2(α) (bez dodatečného předpokladu). 1
|
|
|
Dôkazy bezespornosti aritmetiky
Horská, Anna ; Pudlák, Pavel (vedoucí práce) ; Hrubeš, Pavel (oponent) ; Buss, Samuel (oponent)
Táto práca pozostáva z dvoch častí. Prvá čast sa zaoberá Gentze- novým dôkazom bezespornosti Peanovej aritmetiky (PA), ktorý pochádza z roku 1935. Skúmame hlavne Gentzenovu stratégiu eliminácie rezu, ktorá eliminuje rezy, ktorých premisy majú bezrezové odvodenia. Neberie sa pritom ohl'ad na zložitost' eliminovaného rezu. Naša analýza Gentzenovej stratégie ukázala, že Gentzen vo svojom dôkaze implicitne využíva transfinitnú induk- ciu po Φω(0), kde Φω je Veblenova funkcia s poradovým číslom ω. Jedná sa o horný odhad a hodnota Φω(0) je horný odhad na výšku nekonečných bezrezových odvodení, ktoré Gentzen konštruuje pre sekventy dokazatel'né v PA. V súčasnosti nemáme výsledky o spodnom odhade. Prvá čast' d'alej obsahuje formalizáciu tohto Gentzenovho dôkazu. Na základe nej vidíme, že hore spomínaná transfinitná indukcia je jediný princíp použitý v dôkaze, ktorý nejde formalizovat' v PA. Druhá čast' porovnáva Gentzenovu a Taitovu stratégiu eliminácie rezu v kla- sickej výrokovej logike. Taitova stratégia znižuje tzv. cut-rank odvodenia. Ked'že výroková logika nepoužíva odvodzovacie pravidlá s vlastnými pre- mennými, s tzv. eigenvariables, podarilo sa nám nadefinovat' elimináciu rezu tak, že obe stratégie dávajú v...
|
|
|
Dôkazy bezespornosti aritmetiky
Horská, Anna ; Pudlák, Pavel (vedoucí práce) ; Hrubeš, Pavel (oponent) ; Buss, Samuel (oponent)
Táto práca pozostáva z dvoch častí. Prvá čast sa zaoberá Gentze- novým dôkazom bezespornosti Peanovej aritmetiky (PA), ktorý pochádza z roku 1935. Skúmame hlavne Gentzenovu stratégiu eliminácie rezu, ktorá eliminuje rezy, ktorých premisy majú bezrezové odvodenia. Neberie sa pritom ohl'ad na zložitost' eliminovaného rezu. Naša analýza Gentzenovej stratégie ukázala, že Gentzen vo svojom dôkaze implicitne využíva transfinitnú induk- ciu po Φω(0), kde Φω je Veblenova funkcia s poradovým číslom ω. Jedná sa o horný odhad a hodnota Φω(0) je horný odhad na výšku nekonečných bezrezových odvodení, ktoré Gentzen konštruuje pre sekventy dokazatel'né v PA. V súčasnosti nemáme výsledky o spodnom odhade. Prvá čast' d'alej obsahuje formalizáciu tohto Gentzenovho dôkazu. Na základe nej vidíme, že hore spomínaná transfinitná indukcia je jediný princíp použitý v dôkaze, ktorý nejde formalizovat' v PA. Druhá čast' porovnáva Gentzenovu a Taitovu stratégiu eliminácie rezu v kla- sickej výrokovej logike. Taitova stratégia znižuje tzv. cut-rank odvodenia. Ked'že výroková logika nepoužíva odvodzovacie pravidlá s vlastnými pre- mennými, s tzv. eigenvariables, podarilo sa nám nadefinovat' elimináciu rezu tak, že obe stratégie dávajú v...
|
|
|
Model constructions for bounded arithmetic
Garlík, Michal ; Krajíček, Jan (vedoucí práce) ; Buss, Samuel (oponent) ; Thapen, Neil (oponent)
Název práce: Konstrukce modelů omezené aritmetiky Autor: Michal Garlík Abstrakt: Studujeme konstrukce modelů teorií omezené aritmetiky. Pomocí základních technik teorie modelů podáme nový důkaz Ajtaiovy věty o úplnosti pro nestandardně konečné struktury. Za použití omezené redukované mocniny (zobecnění ultraproduktu) navrhneme dvě nové metody konstrukce modelů ome- zené aritmetiky. První dá nový důkaz Bussovy dosvědčující věty. Druhou metodou ukážeme, že teorie R1 2 je silnější než její varianta strictR1 2 za věrohodného výpo- četně-složitostního předpokladu (existence dostatečně silné jednosměrné permu- tace) a že za stejného předpokladu je teorie PV1 + Σb 1(PV ) − LLIND silnější než PV1 + strictΣb 1(PV ) − LLIND. Pro relativizované teorie dokážeme, že R1 2(α) je silnější strictR1 2(α) (bez dodatečného předpokladu). 1
|
|
|
Complexity theory in Feasible Mathematics
Pich, Ján ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent) ; Buss, Samuel (oponent)
Skúmame dokázateľnosť tvrdení z teórie zložitosti v obmedzenej aritmetike. Za istých zložitostných predpokladov ukážeme, že teórie so slabšími dosvedčovacími vlastnosťami než $S^1_2$ nemôžu dokázať spodné odhady veľkosti $n^k$ na booleovské obvody pre SAT vyjadrené formulou $LB(SAT,n^k)$. Špeciálne, prvorádová teória pravdivých univerzálnych tvrdení v jazyku obsahujúcom symboly pre všetky uniformné $NC^1$ algoritmy nedokazuje $LB(SAT,n^{4kc})$ pre $k\geq 1,c\geq 2$ predpokladajúc existenciu funkcie $f\in SIZE(n^k)$, ktorá nie je aproximovateľná formulami $F_n$ subexponenciálnej veľkosti $2^{O(n^{1/c})}$ so subexponenciálnou výhodou: $P_{x\in\{0,1\}^n}[F_n(x)=f(x)]\geq 1/2+1/2^{O(n^{1/c})}$. Bezpodmienečne, teória $V^0$ nedokazuje kvazipolynomiálne spodné odhady na booleovské obvody pre SAT. Čo sa týka horných odhadov, dokážeme PCP vetu v Cookovej teórii $PV_1$. To zahŕňa formalizáciu $(n,d,\lambda)$-grafov v $PV_1$. Ako dôsledok dostaneme polynomiálne krátke Extended Frege dôkazy tautologií vyjdadrujúcich PCP vetu. Powered by TCPDF (www.tcpdf.org)
|
host ::
RSS.