zbMATH — the first resource for mathematics

NLCertify: a tool for formal nonlinear optimization. (English) Zbl 1434.68640
Hong, Hoon (ed.) et al., Mathematical software – ICMS 2014. 4th international congress, Seoul, South Korea, August 5–9, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8592, 315-320 (2014).
Summary: 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.
For the entire collection see [Zbl 1293.65003].

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
65Y15 Packaged methods for numerical algorithms
90-04 Software, source code, etc. for problems pertaining to operations research and mathematical programming
90C24 Tropical optimization (e.g., max-plus optimization)
90C30 Nonlinear programming
Full Text: DOI arXiv