Полуалгебраические доказательства

Сложность доказательств для логики высказываний — активно развивающаяся область математики. Наличие доказательств, ограниченных по длине полиномом от размера доказываемого утверждения, означало бы равенство сложностных классов NP и coNP. Известны же лишь нижние (и верхние) оценки сложности доказательств для конкретных систем доказательств (и конкретных тавтологий, соответственно).
Первая часть доклада представляет собой введение в эту область и обзор известных систем доказательств и результатов о них.
Вторая часть доклада будет посвящена результатам докладчика (совместным с Д. Ю. Григорьевым и Д. В. Пасечником), касающимся полуалгебраических (т.е. использующих рассуждения о полиномиальных неравенствах) доказательств. Например, вот доказательство принципа Дирихле:
$$ \sum_{k=1}^m\biggl(\sum_{l=1}^{m-1} x_{kl}-1\biggr)+\sum_{l=1}^{m-1}\biggl(\sum_{k=1}^m\biggl(\sum_{k\ne k'=1}^m (1-x_{kl}-x_{k'l})x_{kl}+(x_{kl}^2-x_{kl})(m-2)\biggr)+\biggl(\sum_{k=1}^m x_{kl}-1\biggr)^2\biggr)=-1. $$
(В докладе будет сказано, почему.) Доказательства же этого принципа во многих других системах имеют экспоненциальную (от количества кроликов $m$) длину.