Back to Search Start Over

Verified Real Number Calculations: A Library for Interval Arithmetic.

Verified Real Number Calculations: A Library for Interval Arithmetic.

Authors :
Daumas, Marc
Lester, David
Muñoz, César
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