NLCertify: a tool for formal nonlinear optimization
From MaRDI portal
Publication:2879141
proof assistanthybrid symbolic-numeric certificationmax-plus approximationformal nonlinear optimizationsparse SOS
Packaged methods for numerical algorithms (65Y15) Nonlinear programming (90C30) Software, source code, etc. for problems pertaining to operations research and mathematical programming (90-04) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Tropical optimization (e.g., max-plus optimization) (90C24)
Abstract: NLCertify is a software package for handling formal certification of nonlinear inequalities involving transcendental multivariate functions. The tool exploits sparse semialgebraic optimization techniques with approximation methods for transcendental functions, as well as formal features. Given a box and a transcendental multivariate function as input, NLCertify provides OCaml libraries that produce nonnegativity certificates for the function over the box, which can be ultimately proved correct inside the Coq proof assistant.
Recommendations
- Formal Proofs for Nonlinear Optimization
- Certification of bounds of non-linear functions: the templates method
- Certification of real inequalities: templates and sums of squares
- {\textsc{RealCertify}}: a Maple package for certifying non-negativity
- Dynamics of a parametrically excited system with two forcing terms
Cited in
(7)- Formal Proofs for Nonlinear Optimization
- Certification of real inequalities: templates and sums of squares
- Gposolver: a Matlab/C++ toolbox for global polynomial optimization
- NLCertify
- Dynamics of a parametrically excited system with two forcing terms
- Certification of bounds of non-linear functions: the templates method
- {\textsc{RealCertify}}: a Maple package for certifying non-negativity
This page was built for publication: NLCertify: a tool for formal nonlinear optimization
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879141)
