Proving Bounds on Real-Valued Functions with Computations

DOI10.1007/978-3-540-71070-7_2zbMath1165.68464OpenAlexW1599525342MaRDI QIDQ3541683

Guillaume Melquiond

Publication date: 27 November 2008

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_2

Mathematics Subject Classification ID

Related Items (14)

Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ Axiomatic reals and certified efficient exact real computation ⋮ Proving tight bounds on univariate expressions with elementary functions in Coq ⋮ Affine Arithmetic and Applications to Real-Number Proving ⋮ Unnamed Item ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ Formal verification of numerical programs: from C annotated programs to mechanical proofs ⋮ A certificate-based approach to formally verified approximations ⋮ Multi-Prover Verification of Floating-Point Programs ⋮ Coquelicot: a user-friendly library of real analysis for Coq ⋮ Floating-point arithmetic in the Coq system ⋮ Combining Coq and Gappa for Certifying Floating-Point Programs ⋮ Hardware-Dependent Proofs of Numerical Programs ⋮ Formalization of Bernstein polynomials and applications to global optimization

Uses Software

• Coq
• HOL Light

Cites Work

• Implementing the cylindrical algebraic decomposition within the Coq system
• A Computational Approach to Pocklington Certificates in Type Theory
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Formal Global Optimisation with Taylor Models
• A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
• Theorem Proving in Higher Order Logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proving Bounds on Real-Valued Functions with Computations