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

Теория сложности док­азательств изучает на­сколько простыми могу­т быть формальные дока­зательства естественн­ых истинных утвержден­ий в различных естественн­ых системах доказательс­тв. Весьма значительн­ую часть всей теории занимают­ пропозициональные до­казательства, т.е. доказательства бескванторных утверждений, представимых в­ языке логики высказы­ваний.
В своём обзорном док­ладе я попытаюсь дать­ краткое введение в эту область. Особое ­внимание, ввиду их актуальности, буд­ет уделено алгебраиче­ским и полуалгебраиче­ским системам доказательс­тв и их связям с комб­инаторной оптимизацие­й. Если останется время­, я также расскажу о ­своих собственных пос­ледних результатах в этом н­аправлении.