title = { On the Generation of {P}ositivstellensatz Witnesses in Degenerate Cases },
    author = {Monniaux, David and Corbineau, Pierre},
    month = {aug},
    year = {2011},
    booktitle = {Interactive Theorem Proving (ITP)},
    pages = {249--264},
    volume = {6898},
    team = {SYNC,DCS,PACSS},
    abstract = {One can reduce the problem of proving that a polynomial is nonnegative, or more generally of proving that a system of polynomial inequalities has no solutions, to finding polynomials that are sums of squares of polynomials and satisfy some linear equality (\tgerman{Positivstellensatz}). This produces a \emph{witness} for the desired property, from which it is reasonably easy to obtain a formal proof of the property suitable for a proof assistant such as Coq. The problem of finding a witness reduces to a feasibility problem in semidefinite programming, for which there exist numerical solvers. Unfortunately, this problem is in general not strictly feasible, meaning the solution can be a convex set with empty interior, in which case the numerical optimization method fails. Previously published methods thus assumed strict feasibility; we propose a workaround for this difficulty. We implemented our method and illustrate its use with examples, including extractions of proofs to Coq. },



Publication Sections

Contact | Site Map | Site powered by SPIP 3.0.25 + AHUNTSIC [CC License]

info visites 776493