|
|
(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
|
|
|
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....
|
|
|
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....
|
host ::
RSS.