Formally Verified Approximations of Definite Integrals

Assia Mahboubi 1 Guillaume Melquiond 2 Thomas Sibut-Pinote 1
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : Finding an elementary form for an antiderivative is often a difficult task, so numerical integration has become a common tool when it comes to making sense of a definite integral. Some of the numerical integration methods can even be made rigorous: not only do they compute an approximation of the integral value but they also bound its inaccuracy. Yet numerical integration is still missing from the toolbox when performing formal proofs in analysis. This paper presents an efficient method for automatically computing and proving bounds on some definite integrals inside the Coq formal system. Our approach is not based on traditional quadrature methods such as Newton-Cotes formulas. Instead, it relies on computing and evaluating antiderivatives of rigorous polynomial approximations, combined with an adaptive domain splitting. This work has been integrated to the CoqInterval library.
Type de document :
Communication dans un congrès
Jasmin Christian Blanchette; Stephan Merz. Interactive Theorem Proving, Aug 2016, Nancy, France. 9807, 2016, Lecture Notes in Computer Science. 〈https://itp2016.inria.fr/〉. 〈10.1007/978-3-319-43144-4_17〉
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01289616
Contributeur : Guillaume Melquiond <>
Soumis le : vendredi 27 mai 2016 - 11:07:01
Dernière modification le : jeudi 11 janvier 2018 - 02:01:56
Document(s) archivé(s) le : dimanche 28 août 2016 - 10:41:12

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Jasmin Christian Blanchette; Stephan Merz. Interactive Theorem Proving, Aug 2016, Nancy, France. 9807, 2016, Lecture Notes in Computer Science. 〈https://itp2016.inria.fr/〉. 〈10.1007/978-3-319-43144-4_17〉. 〈hal-01289616v2〉

Partager

Métriques

Consultations de la notice

398

Téléchargements de fichiers

203