Advertisement
Published in:
2014 | OriginalPaper | Chapter
NLCertify: A Tool for Formal Nonlinear Optimization
Author : Victor Magron
Published in: Mathematical Software – ICMS 2014
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.