2014/05/22 by Victor Magron, Magron, Victor
Computer Science · Mathematics · #Polynomial and algebraic computation #Numerical Methods and Algorithms #Advanced Optimization Algorithms Research
paper · doi:10.48550/arxiv.1405.5668
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.