Системы доказательств для языков. Полиномиально ограниченные системы доказальств и класс NP. Языки SAT и UNSAT. Существование полиномиально ограниченной системы доказательств для UNSAT и проблема равенства классов P и NP. Программа Кука.

Разрешающие деревья как ситема доказательств. Принцип Дирихле. Игры для доказательства нижних оценок на глубину. Игры Прувера и Делэера. Асимметричные игры. Точные верхние и нижние оценки на принцип Дирихле.

Текущая версия конспекта тут: https://logic.pdmi.ras.ru/~dmitrits/nsu/pc.pdf