Formal Proofs for Nonlinear Optimization

DOI10.6092/issn.1972-5787/4319zbMath1451.90131arXiv1404.7282MaRDI QIDQ5195260

Stéphane Gaubert, Benjamin Werner, Xavier Allamigeon, Victor Magron

Publication date: 18 September 2019

Full work available at URL: https://arxiv.org/abs/1404.7282

zbMATH Keywords

semidefinite programmingtranscendental functionsproof assistantpolynomial optimization problemsmaxplus approximationsemialgebraic relaxationsFlyspeck projecthybrid symbolic-numeric certificationtemplates method

Mathematics Subject Classification ID

Semidefinite programming (90C22) Nonconvex programming, global optimization (90C26) Nonlinear programming (90C30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (9)

A heuristic method for certifying isolated zeros of polynomial systems ⋮ Duality of sum of nonnegative circuit polynomials and optimal SONC bounds ⋮ Certifying solutions to overdetermined and singular polynomial systems over \(\mathbb{Q}\) ⋮ Polynomials with bounds and numerical approximation ⋮ Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares ⋮ Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials ⋮ Primitive Floats in Coq ⋮ Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems ⋮ Certification of real inequalities: templates and sums of squares

Uses Software

• Coq
• MetiTarski
• SDPA
• PVS
• HOL Light
• Flyspeck

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 11th international conference on geometry and applications
• Boundary value problems in weighted spaces of polyanalytic functions in half-plane
• Floating-point arithmetic in the Coq system
• A numerical evaluation of several stochastic algorithms on selected continuous global optimization test problems
• Max-plus methods for nonlinear control and estimation.
• MetiTarski: An automatic theorem prover for real-valued special functions
• Certification of real inequalities: templates and sums of squares
• Formalization of Bernstein polynomials and applications to global optimization
• Computing sum of squares decompositions with rational coefficients
• A proof of the Kepler conjecture
• A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
• Global Optimization with Polynomials and the Problem of Moments
• Latest Developments in the SDPA Family for Solving Large-Scale SDPs
• Certification of Bounds of Non-linear Functions: The Templates Method
• Special cases
• A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
• Positivity and Optimization for Semi-Algebraic Functions
• On the Generation of Positivstellensatz Witnesses in Degenerate Cases
• GloptiPoly 3: moments, optimization and semidefinite programming
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Formal Global Optimisation with Taylor Models
• The Max-Plus Finite Element Method for Solving Deterministic Optimal Control Problems: Basic Properties and Convergence Analysis
• A two-level approach towards lean proof-checking
• A Max-Plus-Based Algorithm for a Hamilton--Jacobi--Bellman Equation of Nonlinear Filtering
• Optimization of Polynomials on Compact Semialgebraic Sets
• Sums of Squares and Semidefinite Program Relaxations for Polynomial Optimization Problems with Structured Sparsity
• Theorem Proving in Higher Order Logics
• Algebra and Coalgebra in Computer Science
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Topology

This page was built for publication: Formal Proofs for Nonlinear Optimization