Certification of Bounds of Non-linear Functions: The Templates Method

DOI10.1007/978-3-642-39320-4_4zbMath1390.68570arXiv1307.3231OpenAlexW3101257470MaRDI QIDQ2843005

Stéphane Gaubert, Xavier Allamigeon, Victor Magron, Benjamin Werner

Publication date: 9 August 2013

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1307.3231

zbMATH Keywords

semidefinite programmingtranscendental functionsproof assistantpolynomial optimization problemsquadratic cutssemialgebraic relaxationsFlyspeck projecthybrid symbolic-numeric certificationmax-plus approximationtemplates method

Mathematics Subject Classification ID

Related Items (3)

Proving tight bounds on univariate expressions with elementary functions in Coq ⋮ Formal Proofs for Nonlinear Optimization ⋮ Certification of real inequalities: templates and sums of squares

Uses Software

• Coq
• MetiTarski
• SparsePOP
• Intsolver
• Flyspeck

This page was built for publication: Certification of Bounds of Non-linear Functions: The Templates Method