Formalization of Bernstein polynomials and applications to global optimization
From MaRDI portal
Publication:2351165
DOI10.1007/s10817-012-9256-3zbMath1314.68286OpenAlexW1993722858MaRDI QIDQ2351165
Anthony Narkawicz, César A. Muñoz
Publication date: 23 June 2015
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-012-9256-3
global optimizationBernstein polynomialsformal verificationinteractive theorem provingnon-linear arithmetic
Related Items
Dual Certificates and Efficient Rational Sum-of-Squares Decompositions for Polynomial Optimization over Compact Sets, Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems, Automatic dynamic parallelotope bundles for reachability analysis of nonlinear systems, Proving tight bounds on univariate expressions with elementary functions in Coq, Affine Arithmetic and Applications to Real-Number Proving, Formalization of the Lindemann-Weierstrass theorem, Formalization of real analysis: a survey of proof assistants and libraries, Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL, Matrix methods for the tensorial Bernstein form, Coquelicot: a user-friendly library of real analysis for Coq, On exact Reznick, Hilbert-Artin and Putinar's representations, Formal Proofs for Nonlinear Optimization, Theorem of three circles in Coq
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MetiTarski: An automatic theorem prover for real-valued special functions
- Fast construction of constant bound functions for sparse polynomials
- An efficient algorithm for range computation of polynomials using the Bernstein form
- Semidefinite programming relaxations for semialgebraic problems
- Application of Bernstein expansion to the solution of control problems
- Taylor forms -- use and limits.
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases
- A formal study of Bernstein coefficients and polynomials
- Implementing the cylindrical algebraic decomposition within the Coq system
- Verifying Nonlinear Real Formulas Via Sums of Squares
- Proving Bounds on Real-Valued Functions with Computations
- Algorithm 852
- Formal Global Optimisation with Taylor Models
- Combined Decision Techniques for the Existential Theory of the Reals
- Verified Real Number Calculations: A Library for Interval Arithmetic
- Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
- Automated Deduction – CADE-20
- Correct Hardware Design and Verification Methods
