Теория сложности доказательств

Теория сложности доказательств изучает насколько простыми могут (или не могут) быть формальные доказательства истинных утверждений в различных естественных системах доказательств. Классы рассматриваемых утверждений и систем могут существенно варьироваться в зависимости от контекста, что определяет целый ряд неожиданных и важных взаимосвязей между теорией сложности доказательств и многими областями в математике и компьютерных науках. Весьма значительную часть всей теории занимают пропозициональные доказательства, т.е. доказательства бескванторных утверждений, представимых в языке логики высказываний.
В своём обзорном докладе я попытаюсь дать по необходимости краткое введение в эту последнюю область. Две темы, которым я планирую уделить особое внимание ввиду их актуальности, таковы:
1. Система резолюций и практические алгоритмы для выполнимости булевых формул. 2. Алгебраические и полуалгебраические системы доказательств и комбинаторная оптимизация.
Если останется время, я также расскажу о своих собственных последних результатах в этих направлениях.