salle A. Turing CE4
7 February 2014 - 14h00
Formal Certificates for Nonlinear Inequalities
by Victor Magron from LAAS
Abstract: In this talk, I will present a general framework to provide valid
certificates for nonlinear real inequalities, defined by semialgebraic or
transcendental expressions and to prove the correctness of these
certificates inside the Coq proof system.
The application range for such a tool is widespread; for instance Hales\'
proof of Kepler\'s conjecture involves thousands of nonlinear inequalities.
The functions we are dealing with are nonlinear and involve semialgebraic
operations as well as some transcendental functions like cos, arctan, exp,
etc. Different approximation methods allow to relax the original problem
into a semialgebraic optimization problem. It leads to polynomial
optimization problems which are efficiently solved by sparse sums of
squares relaxations.
Finally, I will explain how to extend this method to tackle multiobjective
optimization problems.
