Moscow Mathematical Journal
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Mosc. Math. J.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Moscow Mathematical Journal, 2002, Volume 2, Number 4, Pages 647–679
DOI: https://doi.org/10.17323/1609-4514-2002-2-4-647-679
(Mi mmj67)
 

This article is cited in 35 scientific papers (total in 35 papers)

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
Full-text PDF Citations (35)
References:
Abstract: It is a known approach to translate propositional formulas into systems of polynomial inequalities and consider proof systems for the latter. The well-studied proof systems of this type are the Cutting Plane proof system (CP) utilizing linear inequalities and the Lovász–Schrijver calculi (LS) utilizing quadratic inequalities. We introduce generalizations ${\rm LS}^d$ of LS that operate on polynomial inequalities of degree at mos $d$.
It turns out that the obtained proof systems are very strong. We construct polynomial-size bounded-degree ${\rm LS}^d$ proofs of the clique-coloring tautologies (which have no polynomial-size CP proofs), the symmetric knapsack problem (which has no bounded-degree Positivstellensatz calculus proofs), and Tseitin's tautologies (which are hard for many known proof systems). Extending our systems with a division rule yields a polynomial simulation of CP with polynomially bounded coefficients, while other extra rules further reduce the proof degrees for those examples.
Finally, we prove lower bounds on the Lovász–Schrijver ranks and on the size and the “Boolean degree” of Positivstellensatz calculus refutations. We use the latter bound to obtain an exponential lower bound on the size of Positivstellensatz calculus,
textit{static} ${\rm LS}^d$, and tree-like ${\rm LS}^d$ refutations.
Key words and phrases: Computational complexity, propositional proof system.
Received: March 24, 2002
Bibliographic databases:
MSC: Primary 03F20; Secondary 68Q17
Language: English
Citation: D. Yu. Grigor'ev, E. A. Hirsch, D. V. Pasechnik, “Complexity of semialgebraic proofs”, Mosc. Math. J., 2:4 (2002), 647–679
Citation in format AMSBIB
\Bibitem{GriHirPas02}
\by D.~Yu.~Grigor'ev, E.~A.~Hirsch, D.~V.~Pasechnik
\paper Complexity of semialgebraic proofs
\jour Mosc. Math.~J.
\yr 2002
\vol 2
\issue 4
\pages 647--679
\mathnet{http://mi.mathnet.ru/mmj67}
\crossref{https://doi.org/10.17323/1609-4514-2002-2-4-647-679}
\mathscinet{http://mathscinet.ams.org/mathscinet-getitem?mr=1986085}
\zmath{https://zbmath.org/?q=an:1027.03044}
\isi{https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=Publons&SrcAuth=Publons_CEL&DestLinkType=FullRecord&DestApp=WOS_CPL&KeyUT=000208593600002}
Linking options:
  • https://www.mathnet.ru/eng/mmj67
  • https://www.mathnet.ru/eng/mmj/v2/i4/p647
  • This publication is cited in the following 35 articles:
    Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Moscow Mathematical Journal
    Statistics & downloads:
    Abstract page:260
    References:65
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024