RUS  ENG
Полная версия
ЖУРНАЛЫ // Moscow Mathematical Journal // Архив

Mosc. Math. J., 2002, том 2, номер 4, страницы 647–679 (Mi mmj67)

Эта публикация цитируется в 35 статьях

Complexity of semialgebraic proofs

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

D. Yu. Grigor'eva, E. A. Hirschb, D. V. Pasechnikcd

a University of Rennes 1
b St. Petersburg Department of V. A. Steklov Institute of Mathematics, Russian Academy of Sciences
c Delft University of Technology
d Johann Wolfgang Goethe-Universität

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

MSC: Primary 03F20; Secondary 68Q17

Статья поступила: 24 марта 2002 г.

Язык публикации: английский

DOI: 10.17323/1609-4514-2002-2-4-647-679



Реферативные базы данных:


© МИАН, 2024