Proving tight bounds on univariate expressions with elementary functions in Coq
type: Item
instance of: scholarly article
title: Proving tight bounds on univariate expressions with elementary functions in Coq
zbMATH Open document ID: 1386.68151
author: Érik Martin-Dorel
author: Guillaume Melquiond
published in: Journal of Automated Reasoning
publication date: 2016-10-27T00:00:00Z
full work available at URL: article.pdf
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 41A58
Mathematics Subject Classification ID: 65G50
zbMATH DE Number: 6644464
zbMATH Keywords: interval arithmetic
zbMATH Keywords: formal proof
zbMATH Keywords: decision procedure
zbMATH Keywords: Coq proof assistant
zbMATH Keywords: floating-point arithmetic
zbMATH Keywords: nonlinear arithmetic
describes a project that uses: MetiTarski
describes a project that uses: PVS
describes a project that uses: Flocq
describes a project that uses: Coq
describes a project that uses: Sollya
MaRDI profile type: Publication
OpenAlex ID: W1915348541
cites work: MetiTarski: An automatic theorem prover for real-valued special functions
cites work: Certification of Bounds of Non-linear Functions: The Templates Method
cites work: Formalization of Bernstein polynomials and applications to global optimization
cites work: Horner's rule for interval evaluation revisited
cites work: Efficient and accurate computation of upper bounds of approximation errors
cites work: Sollya: An Environment for the Development of Numerical Codes
cites work: Verified Real Number Calculations: A Library for Interval Arithmetic
cites work: Q4808034
cites work: Verifying Nonlinear Real Formulas Via Sums of Squares
cites work: Proving Bounds on Real-Valued Functions with Computations
cites work: Floating-point arithmetic in the Coq system
cites work: Q5566070
cites work: Handbook of Floating-Point Arithmetic
cites work: Table-driven implementation of the exponential function in IEEE floating-point arithmetic
cites work: Fast evaluation of elementary mathematical functions with correctly rounded last bit
DOI: 10.1007/S10817-015-9350-4
Recommended article: Proof by computation in the Coq system
Recommended article: Quantitative continuity and Computable Analysis in Coq
Recommended article: A Coq formalization of Lebesgue induction principle and Tonelli's theorem
Recommended article: Theorem Proving in Higher Order Logics
Recommended article: Q5875441
Recommended article: Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls
Recommended article: A Coq formalization of Lebesgue integration of nonnegative functions
Recommended article: Extending a Resolution Prover for Inequalities on Elementary Functions
Recommended article: A Proof System for MSVL Programs in Coq
Recommended article: A formal proof in Coq of Lasalle's invariance principle
description: scientific article; zbMATH DE number 6644464