Complexity of null- and Positivstellensatz proofs

D Grigoriev, N Vorobjov

Research output: Contribution to journalArticle

44 Citations (Scopus)

Abstract

We introduce two versions of proof systems dealing with systems of inequalities: Positivstellensatz refutations and Positivstellensatz calculus. For both systems we prove the lower bounds on degrees and lengths of derivations for the example due to Lazard, Mora and Philippon. These bounds are sharp, as well as they are for the Nullstellensatz refutations and for the polynomial calculus. The bounds demonstrate a gap between the Null- and Positivstellensatz refutations on one hand, and the polynomial calculus and Positivstellensatz calculus on the other. (C) 2002 Elsevier Science B.V. All rights reserved.
Original languageEnglish
Pages (from-to)153-160
Number of pages8
JournalAnnals of Pure and Applied Logic
Volume113
Issue number1-3
Publication statusPublished - 2002

    Fingerprint

Cite this