Formally Verified Approximations of Definite Integrals

Autor: Thomas Sibut-Pinote, Assia Mahboubi, Guillaume Melquiond
Přispěvatelé: GALLINETTE ( GALLINETTE ), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Laboratoire des Sciences du Numérique de Nantes ( LS2N ), Université de Nantes ( UN ) -École Centrale de Nantes ( ECN ) -Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ) -Université de Nantes ( UN ) -École Centrale de Nantes ( ECN ) -Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ), Symbolic Special Functions : Fast and Certified ( SPECFUN ), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ), Certified Programs, Certified Tools, Certified Floating-Point Computations ( TOCCATA ), Laboratoire de Recherche en Informatique ( LRI ), Université Paris-Sud - Paris 11 ( UP11 ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ) -Université Paris-Sud - Paris 11 ( UP11 ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ) -Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique ( Inria ), ANR-14-CE25-0018,Fast Relax,Fast Reliable Approximation ( 2014 ), Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Symbolic Special Functions : Fast and Certified (SPECFUN), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, ANR-14-CE25-0018,Fast Relax,Approximation rapide et fiable(2014), Jasmin Christian Blanchette, Stephan Merz, Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique)
Jazyk: angličtina
Rok vydání: 2018
Předmět:
[ MATH.MATH-CA ] Mathematics [math]/Classical Analysis and ODEs [math.CA]
Computer science
0102 computer and information sciences
02 engineering and technology
[MATH.MATH-CA]Mathematics [math]/Classical Analysis and ODEs [math.CA]
definite integrals
interval arithmetic
Mathematical proof
01 natural sciences
Antiderivative
Formal proof
[ INFO.INFO-AO ] Computer Science [cs]/Computer Arithmetic
Interval arithmetic
Order of integration (calculus)
Artificial Intelligence
formal proof
Improper integral
0202 electrical engineering
electronic engineering
information engineering
Calculus
polynomial approximations
Mathematics
numeric computations
Real analysis
Improper integrals
[INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic
Constant of integration
Mathematical analysis
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
decision procedure
Quadrature (mathematics)
Numerical integration
Computational Theory and Mathematics
010201 computation theory & mathematics
[ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO]
real analysis
Software
Zdroj: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2018, pp.1-20. 〈10.1007/s10817-018-9463-7〉
Journal of Automated Reasoning, Springer Verlag, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩
Interactive Theorem Proving
Interactive Theorem Proving, Aug 2016, Nancy, France. ⟨10.1007/978-3-319-43144-4_17⟩
Interactive Theorem Proving ISBN: 9783319431437
ITP
Journal of Automated Reasoning, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩
ISSN: 0168-7433
1573-0670
Popis: International audience; 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. Our approach also handles improper integrals, provided that a factor of the integrand belongs to a catalog of identified integrable functions. This work has been integrated to the CoqInterval library.
Databáze: OpenAIRE
Externí odkaz: