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 (13)
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
This page was built for publication: Formalization of Bernstein polynomials and applications to global optimization
