Back to Search
Start Over
Verified Real Number Calculations: A Library for Interval Arithmetic.
Verified Real Number Calculations: A Library for Interval Arithmetic.
- Source :
-
IEEE Transactions on Computers . Feb2009, Vol. 58 Issue 2, p226-237. 12p. - Publication Year :
- 2009
-
Abstract
- 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. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 00189340
- Volume :
- 58
- Issue :
- 2
- Database :
- Academic Search Index
- Journal :
- IEEE Transactions on Computers
- Publication Type :
- Academic Journal
- Accession number :
- 37374585
- Full Text :
- https://doi.org/10.1109/TC.2008.213