Formally verified approximations of definite integrals

Assia Mahboubi, Guillaume Melquiond*, Thomas Sibut-Pinote

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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.

Original languageEnglish
Title of host publicationInteractive Theorem Proving - 7th International Conference, ITP 2016, Proceedings
EditorsJasmin Christian Blanchette, Stephan Merz
PublisherSpringer Verlag
Pages274-289
Number of pages16
ISBN (Print)9783319431437
DOIs
Publication statusPublished - 1 Jan 2016
Externally publishedYes
Event7th International Conference on Interactive Theorem Proving, ITP 2016 - Nancy, France
Duration: 22 Aug 201625 Aug 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9807 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Conference on Interactive Theorem Proving, ITP 2016
CountryFrance
CityNancy
Period22/08/1625/08/16

Fingerprint Dive into the research topics of 'Formally verified approximations of definite integrals'. Together they form a unique fingerprint.

Cite this