\( \def\sc#1{\dosc#1\csod} \def\dosc#1#2\csod{{\rm #1{\small #2}}} \def\nlcertify{\textrm{NLCertify}} \def\xb{\mathbf{x}} \def\ocaml{\sc{OCAML}} \def\coq{\sc{COQ}} \def\hol{\sc{HOL-LIGHT}} \)


$\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 $K := [a_1, b_1] \times \dots \times [a_n, b_n]$ and an $n$-variate function $f$ as input, $\nlcertify$ provides $\ocaml$ libraries that produce nonnegativity certificates for $f$ over $K$. The certificate can be ultimately verified inside the $\coq$ theoretical prover.

Install it or have a look at the examples.