Деревья расщепления, игры Прувера и Делэера. Нижняя оценка 2^n на
принцип Дирихле.
Асимметричные игры Прувера и Делэера. Оптимальная оценка на принцип Дирихле
для деревьев расщепления.
Резолюционная система доказательств. Корректность и полнота.
Древовидная резолюция и расщепление. Игры Пудлака и размер резолюционных
доказательств.
Нижняя оценка на принцип Дирихле в резолюционной системе доказательств.
Ширина резолюционного доказательства. Связь между доказательством и шириной
--- теорема Бен-Сассона и Вигдерсона.
Цейтинские формулы, нижняя оценка на цейтинские формулы в резолюциях.
Нижние оценки на принцип Дирихле с помощью оценки на ширину, графовая
версия принципа Дирихле.
Игры Атсериаса и Долмау и комбинаторная характеризация ширины.
Память резолюционных систем доказательств. Связь ширины и ClauseSpace.
Оптимальная нижняя оценка на TotalSpace. Игры, нижняя оценка на битовый принцип Дирихле, нижняя оценка с помощью
ксорификации.
PC и PCR, корректность и полнота. Нижняя оценка на размер следует из нижней оценки на степень.
Нижняя оценка на степень вывода в PC для случайных формул.
Cutting Plane, моделирование резолюции, верхняя оценка на принцип Дирихле. Интерполяция,
построение монотонной вещественной схемы для интерполянта по доказательству.
CDCL-солверы. Модель, оценка времени работы через ширину резолюционного доказательства.
Оптимальные и p-оптимальные системы доказательств. Теорема Месснера.
Дизъюнктные NP-пары, каноническая NP-пара для системы доказательств. Оптимальная система доказательств и полная NP-пара.
Автоматизируемость. Отделимость канонической NP-пары и слабая автоматизируемость.
Системы Фреге, их эквивалентность. Расширенные системы Фреге. Разделение древовидной и обычной резолюции.