Original title:
Těžké tautologie
Translated title:
Těžké tautologie
Authors:
Pich, Ján ; Krajíček, Jan (advisor) ; Pudlák, Pavel (referee) Document type: Master’s theses
Year:
2011
Language:
eng Abstract:
[eng][cze] We investigate the unprovability of NP$\not\subseteq$P/poly in various fragments of arithmetic. The unprovability is usually obtained by showing hardness of propositional formulas encoding superpolynomial circuit lower bounds. Firstly, we discuss few relevant techniques and known theorems. Namely, natural proofs, feasible interpolation, KPT theorem, iterability, gadget generators etc. Then we prove some original results. We show the unprovability of superpolynomial circuit lower bounds for systems admitting certain forms of feasible interpolation (modulo a hardness assumption) and for systems roughly described as tree-like Frege systems working with formulas using only a small fraction of variables of the statement that is supposed to be proved. These results are obtained by proving the hardness of the Nisan-Wigderson generators in corresponding proof systems.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.
Keywords:
circuit lower bounds; generators; Nisan-Wigderson; proof complexity; booleovské obvody; důkazová složitost; Nisan-Wigderson generátor
Institution: Charles University Faculties (theses)
(web)
Document availability information: Available in the Charles University Digital Repository. Original record: http://hdl.handle.net/20.500.11956/35860