2014 | OriginalPaper | Buchkapitel
NLCertify: A Tool for Formal Nonlinear Optimization
verfasst von : Victor Magron
Erschienen in: Mathematical Software – ICMS 2014
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.