Formal Proofs for Nonlinear Optimization

Formal Proofs for Nonlinear Optimization

We present a formally verified global optimization framework. Given a semialgebraic or transcendental function f and a compact semialgebraic domain K, we use the nonlinear maxplus template approximation algorithm to provide a certified lower bound of f over K.This method allows to bound in a modular...

Full description

Bibliographic Details
Main Authors: Victor Magron, Xavier Allamigeon, Stéphane Gaubert, Benjamin Werner
Format: Article
Language:English
Published: University of Bologna 2015-01-01
Series:Journal of Formalized Reasoning
Subjects:
Polynomial Optimization Problems
Hybrid Symbolic-numeric Certification
Semidefinite Programming
Transcendental Functions
Semialgebraic Relaxations
Flyspeck Project
Maxplus Approximation
Templates Method
Proof Assistant
Online Access:http://jfr.unibo.it/article/view/4319

Internet

http://jfr.unibo.it/article/view/4319

Similar Items