Issue No.02 - February (2009 vol.58)
Marc Daumas , ELIAUS, UPVD, Perpignan
David Lester , University of Manchester, Manchester
Céar Muñoz , National Institute of Aerospace, Hampton
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2008.213
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations take place in an algebraic setting. In order to reduce the dependency effect of interval arithmetic, we integrate two techniques: interval splitting and Taylor series expansions. This pragmatic approach has been developed, and formally verified, in a theorem prover. The formal development also includes a set of customizable strategies to automate proofs involving explicit calculations over real numbers. Our ultimate goal is to provide guaranteed proofs of numerical properties with minimal human theorem-prover interaction.
Real number calculations, interval arithmetic, proof checking, theorem proving.
Marc Daumas, David Lester, Céar Muñoz, "Verified Real Number Calculations: A Library for Interval Arithmetic", IEEE Transactions on Computers, vol.58, no. 2, pp. 226-237, February 2009, doi:10.1109/TC.2008.213