NLCertify: a tool for formal nonlinear optimization

DOI10.1007/978-3-662-44199-2_49zbMATH Open1434.68640arXiv1405.5668OpenAlexW1787747790MaRDI QIDQ2879141FDOQ2879141

Authors: Victor Magron 

Publication date: 8 September 2014

Published in: Mathematical Software – ICMS 2014 (Search for Journal in Brave)

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.

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

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

zbMATH Keywords

proof assistanthybrid symbolic-numeric certificationmax-plus approximationformal nonlinear optimizationsparse SOS

Mathematics Subject Classification ID

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)

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

Uses Software

• Coq
• SparsePOP
• GloptiPoly
• YALMIP
• OCaml
• Sollya

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)