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.