On the Generation of Positivstellensatz Witnesses in Degenerate Cases

Details On the Generation of Positivstellensatz Witnesses in Degenerate Cases On the Generation of Positivstellensatz Witnesses in Degenerate Cases

2011-05-23

arxiv.org/abs/1105.4421v1

Interactive Theorem Proving, Nijmegen : Pays-Bas (2011)

Mathematics

Logic

To appear in ITP 2011

Scientific paper

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 (Positivstellensatz). This produces a 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.

Affiliated with

Also associated with

No associations

Rating

On the Generation of Positivstellensatz Witnesses in Degenerate Cases does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with On the Generation of Positivstellensatz Witnesses in Degenerate Cases, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On the Generation of Positivstellensatz Witnesses in Degenerate Cases will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-22116