Complexity of semialgebraic proofs

Кодирование пропозициональных формул в виде систем полиномиальных неравенств и рассмотрение систем доказательств для последних – известный подход. Хорошо изучены следующие системы подобного типа: секущая плоскость (CP), известная также как исчисление Гомори, использующая линейные неравенства, и исчисления Ловаса–Шрайвера (LS), использующие квадратичные неравенства. Мы вводим обобщения ${\rm LS}^d$ системы LS, оперирующие полиномиальными неравенствами степени не более $d$.
Оказывается, что эти системы весьма сильны. Мы показываем, что в системе ${\rm LS}^d$ имеются доказательства полиномиальной длины и ограниченной степени для тавтологий “клика-раскраска” (не имеющих CP-доказательств полиномиальной длины), для симметричного варианта задачи о рюкзаке (не имеющей доказательств ограниченной длины в Positivstellensatz Calculus), и для цейтинских тавтологий (трудных для многих известных систем доказательств). Расширение наших систем правилом деления дает возможность моделирования CP с полиномиально ограниченными коэффициентами за полиномиальное время; другие дополнительные правила дают дальнейшее понижение степеней доказательств для указанных задач.
Наконец, нами доказываются нижние оценки на ранг в исчислениях Ловаса–Шрайвера и на длину и “булеву степень” опровержений в Positivstellensatz Calculus. Последняя используется для получения нижних оценок на длину статических и древовидных ${\rm LS}^d$-доказательств.