Proving tight bounds on univariate expressions with elementary functions in Coq
From MaRDI portal
Publication:331615
DOI10.1007/s10817-015-9350-4zbMath1386.68151MaRDI QIDQ331615
Érik Martin-Dorel, Guillaume Melquiond
Publication date: 27 October 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01086460/file/article.pdf
interval arithmetic; floating-point arithmetic; formal proof; decision procedure; nonlinear arithmetic; Coq proof assistant
65G50: Roundoff error
41A58: Series expansions (e.g., Taylor, Lidstone series, but not Fourier series)
Uses Software