Proving Bounds on Real-Valued Functions with Computations
From MaRDI portal
Publication:3541683
DOI10.1007/978-3-540-71070-7_2zbMath1165.68464OpenAlexW1599525342MaRDI QIDQ3541683
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
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
