Sylabus a literatura k prednasce

"Logika a slozitost", Jan Krajicek

Kod predmetu: NALG128 (letni semestr).
Kona se: ctvrtek 12.20, seminarni mistnost KA.

Studentsky logicky seminar.

Teorie vypocetni slozitosti a cela teoreticka informatika se vyvinula z matematicke logiky, z problemu studovanych v souvislosti se zaklady matematiky v prvni polovine 20.stoleti. Rada fundamentalnich problemu z teorie slozitosti byla nejprve formulovana jako problem v matematicke logice a rada pojmu a metod teorie slozitosti maji pocatek v matematicke logice. Pristup matematicke logiky je alternativou k prevazne kombinatorickemu videni problemu, ktere dnes prevazuje, a v nekterych oblastech slozitosti dava nejhlubsi porozumeni veci.

Sylabus:

  • Entscheidungsproblem, problem bezespornosti matematiky, axiom vyberu. Hilbert, Godel, Church, Turing, Kleene, ... . "Finitni verse" a souvislosti s P/NP, NP/coNP a jednosmernymi funkcemi.

  • Spektrum problem (Scholz 1952 / Asser 1953), Godeluv dopis von Neumannovi 1956
    (prelozen v Sipserove clanku o P/NP nebo v uvodu me a Cloteho knihy - je v knihovne MFF) . Souvisejici clanek S.Busse.

  • Casova slozitost algoritmu, tridy vypocetni slozitosti. Hlavni problemy.

  • Deskriptivni slozitost: definovatelnost v konecnych strukturach. Faginova veta. Problem spektra podrobne.

  • Prevod splnitelnosti existencnich SO vet na SAT (vyrokova splnitelnost).

  • Polynomialni cas: neadekvatnost FO logiky. Operator nejmensiho pevneho bodu, veta Immermanna a Vardiho.

  • Immerman-Szelepcsenyi veta: NL = coNL (dukaz v podani D.Kozena), logika FO + positivni TC (transitive closure).

  • Jazyk PA a jazyk omezene aritmetiky S_2. Omezene formule (Smullyan 1961, Buss 1986), hierarchie E_1,... a Sigma^b_1, ... . E_1 obsahuje NP uplnou mnozinu (Adleman - Manders). Problem kolapsu, veta Wilkieho a Woodse.

  • Jazyk binarnich slov, rudimentarni mnoziny RUD (Smullyan) a podtridy: SRUD, RUD^+ a strRUD. Rudimentarni funkce, Bennettovo lemma.

  • LinH (Wrathall 1978) a PH (Stockmeyer 1977). LinH = RUD (Wratthall) a RUD = Delta_0 (Bennet), PH = Sigma^b_{\infty} (Buss).

  • Graf umocnovani v RUD (Bennett), Nepomnjascij veta, s dusledkem: L cast Delta_0.

  • Cobhamova charakterizace polynomialnych funkci, jejich konecna baze (Muchnik).

  • Kodovani posloupnosti. Sekvencni teorie.

  • Slozitost dukazu: jak overime dukaz, je dukaz pouzivajici slabsi axiomy lepsi nez dukaz pouzivajici silnejsi axiomy, jak overime pravdivost axiomu, lze z dukazu ziskat vypocetni informaci, ... ?

  • Universalni teorie, priklad: DeMillo-Lipton teorie PT a jeji vady. Hebrandova veta pro AE formule, Statmanuv spodni odhad na velikost Hebrandovske disjunkce. Interpretace termu jako dosvedcovacich funkci.

  • Otevrena (p-time) indukce v PT. Mnozina PT-dokazatelne v NP \cap coNP je jiz v P. Nedokazatelnost v PT (podminena hypotezami ze slozitosti): uplnosti vyrokoveho poctu, existence kolizi v hashovacich funkcich ci existence vzoru u one-way permutace. Prechod od dukazu NP-svedku pro Primes k p-time algoritmu pro Primes.

  • Herbrandova veta pro AEA formule. Interpretace interaktivnimi Student/Teacher vypocty.

  • Student/Teacher vypocet kliky maximalni velikosti v grafu a obecne svedka maximalni velikosti.

  • Nedokazatelnost existence maximalniho svedka v PT (za podminky, ze NP nema polynomialni obvody)

  • IND a PIND (p-IND) pro E_1 formule. Dosvedcovani E_1-PIND polynomialnimi funkcemi a konservativita na TP. Nedokazatelnost E_1-PIND v TP (podminena neexistenci polynomialnich obvodu pro SAT)).

  • PLS (poly local search) vyhledavaci problemy. Dosvedcovani E_1-IND a podminena separace od E_1-PIND.

  • Cookova teorie PV a Bussovy teorie S^i_2 a T^i_2..

  • Dosvedcovaci vety pro PV, S^1_2 a T^1_2.

  • Hierarchive teorii S^i_2, teorie IDelta_0 a problem konecne axiomatizovatelnosti. Souvislost s kolapsem polynomialni hierarchie.

  • Delta_0-PHP a problem jeho dokazatelnosti, slabe PHP (WPHP).

  • Dukazy universalnich dusledku v universalnich teoriich, vyrokove dukazy z Herbrandovy vety.

  • Simulace dukazu v teoriich v jazyce PT ci PV posloupnosti kratkych vyrokovych dukazu. Extended Frege system EF a Extended Resolution ER. Priklad teorie PV. Poznamky.

  • Dukazove systemy pro vyrokovou logiku (Cook-Reckhow). Souvislost s NP vs. coNP problemem. P-simulace. Poznamky.

  • Vyrokove preklady dukazu teorie IDelta_0(R).

  • Problem dokazatelnosti PHP a odpovidajici konstrukce modelu (forma forcingu).

  • Pokrocilejsi temata (zbude-li cas): zaklady dukazove slozitosti, finitni Godelova veta, dokazatelnost spodnich odhadu na obvody a generatory pseudonahodnych cisel (Razborov-Rudich), konstrukce tezkych tautologii, ... .

    Literatura (postupne budu doplnovat):

  • Sanjeev Arora a Boaz Barak, "Complexity Theory: A Modern Approach", rukopis knihy.

  • S.R.Buss, "On Gödel's theorems on lengths of proofs II: Lower bounds for recognizing k symbol provability", in: Feasible Mathematics II, P. Clote and J. Remmel (eds), Birkhauser, 1995, pp. 57-90.

  • S.Buss a J.Krajicek: "An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic", Proceedings of the London Mathematical Society, 69(3), (1994), pp.1-21.

  • P.Clote a J.Krajicek (eds), Arithmetic, Proof Theory, and Computational Complexity", Oxford U. press, (1993).

  • E.Graedel, Finite Model Theory and Descriptive Complexity (kapitola v knize)

  • P.Hajek a P.Pudlak: "Metamathematics of First-Order Arithmetic", Perspectives in Mathematical Logic, Volume 3 Springer-Verlag, 1998. [cast C je o omezene aritmetice]

  • N. Immerman, Nondeterministic space is closed under complementation, SIAM Journal on Computing 17, 1988, pp. 935-938.

  • J.Krajicek, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, (1995).

  • J.Krajicek, Propositional proof complexity I. a Proof complexity and arithmetic, dvoje skripta.

  • J.Krajicek, From feasible proofs to feasible computations, to app. CSL 2010.

  • J.Krajicek, P.Pudlak a G. Takeuti: "Bounded Arithmetic and the Polynomial Hierarchy", Annals of Pure and Applied Logic, 52, (1991), pp. 143-153.

  • Martin Otto, Finite Model Theory, skripta.

  • M.Sipser, "The history and status of the P versus NP question", Proceedings of the 24th annual ACM symposium on Theory of computing, (1992), pp.603 - 618.

  • R. Szelepcsenyi, The method of forcing for nondeterministic automata, Bulletin of the EATCS 33, 1987, pp. 96-100.