NLCertify: A Tool for Formal Nonlinear Optimization
Mathematical Software
2014-05-23 v1 Logic in Computer Science
Optimization and Control
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.
Cite
@article{arxiv.1405.5668,
title = {NLCertify: A Tool for Formal Nonlinear Optimization},
author = {Victor Magron},
journal= {arXiv preprint arXiv:1405.5668},
year = {2014}
}
Comments
6 pages, 2 figures