Эта публикация цитируется в
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