Formally verified approximations of definite integrals

DOI10.1007/s10817-018-9463-7zbMath1468.68301OpenAlexW2791728102WikidataQ130093741 ScholiaQ130093741MaRDI QIDQ1722649

Guillaume Melquiond, Thomas Sibut-Pinote, Assia Mahboubi

Publication date: 18 February 2019

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

Full work available at URL: https://hal.inria.fr/hal-01630143v2/file/main.pdf

zbMATH Keywords

real analysisinterval arithmeticpolynomial approximationsformal proofdecision proceduredefinite integralsimproper integralsnumeric computations

Mathematics Subject Classification ID

Interval and finite arithmetic (65G30) Numerical integration (65D30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Mathematics and the formal turn ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ A certificate-based approach to formally verified approximations ⋮ Verified interactive computation of definite integrals

Uses Software

• Coq
• Octave
• Coquelicot
• Coq Interval

Cites Work

• Unnamed Item
• Proving tight bounds on univariate expressions with elementary functions in Coq
• A computer-verified monadic functional implementation of the integral
• Double bubbles minimize
• Coquelicot: a user-friendly library of real analysis for Coq
• Formally Verified Approximations of Definite Integrals
• Verification methods: Rigorous results using floating-point arithmetic
• Introduction to Interval Analysis
• Adaptive, Self-Validating Numerical Quadrature
• The Picard Algorithm for Ordinary Differential Equations in Coq

This page was built for publication: Formally verified approximations of definite integrals