Issue No. 02 - February (2009 vol. 58)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2008.213
Céar Muñoz , National Institute of Aerospace, Hampton
Marc Daumas , ELIAUS, UPVD, Perpignan
David Lester , University of Manchester, Manchester
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.
Céar Muñoz, Marc Daumas, David Lester, "Verified Real Number Calculations: A Library for Interval Arithmetic", IEEE Transactions on Computers, vol. 58, no. , pp. 226-237, February 2009, doi:10.1109/TC.2008.213