Однопроходные ветвящиеся программы как система доказательств. Эквивалентность регулярных резолюций и однопроходных ветвящихся программ. Эквивалентность разрешающих деревьев и древовидных резолюций.

Ширина резолюционных доказательств. Цейтинские формулы и их свойства, нижняя оценка на ширину через расширительную способность (e(G)).

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