Studentsky logicky seminar

Literatura k tematu "slozitost resoluce" (jaro'09):



Texty na webu (postupne budu doplnovat):

  • Zakladni definice (a trocha historie), Tseitinova limited extension, korektnost, uplnost, priklad PHP. Cook-Reckhow definice dukazoveho systemu, hlavni problem o delkach dukazu, souvislost s NP vs. coNP. DPLL a stromove resolucni dukazy. Prvnich cca 12 stranek v mych skriptech.

  • Spodni odhad pro PHP v R: Buss-Turan (presentace a zobecneni Hakenova dukazu).

  • Spodni odhad pro stromovou resoluci R^*: str. 13 - 18 v mych skriptech.

  • Postacujici podminka pro spodni odhady pro R^* v jazyce t.modelu:
    V.3.2 v me clanku a diplomka T.Auera (Complexity of propositional proofs in resolution, 2001) na FF UK.

  • Metoda nahodnych restrikci. Relativizace kombinatorickych principu: Dantchev - Riis (sekce 2 a 4).

  • Sire (width) resolucnich dukazu a trade-off s velikosti: Ben-Sasson - Wigderson, a aplikace.

  • Sire a oblazkove hry: Atserias - Dalmau.

  • Prostorova slozitost resolucnich dukazu: Esteban - Toran a Esteban.

  • Zobecneni resoluce: rozsirena resoluce ER (clanek Cook 1975, Sekce 5) a system R^+ (Sekce 1) a podsystemy R(f).

  • Tzv. feasible interpolation pro resoluci a aplikace.