Formal Proofs for Nonlinear Optimization
From MaRDI portal
Publication:5195260
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
semidefinite programmingtranscendental functionsproof assistantpolynomial optimization problemsmaxplus approximationsemialgebraic relaxationsFlyspeck projecthybrid symbolic-numeric certificationtemplates method
Semidefinite programming (90C22) Nonconvex programming, global optimization (90C26) Nonlinear programming (90C30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
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
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
