@inproceedings{MC11,
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. },
}
