Verified Real Number Calculations: A Library for Interval Arithmetic
| dc.creator | Daumas, Marc | |
| dc.creator | Lester, David | |
| dc.creator | Muñoz, César | |
| dc.date | 2007-08-28 | |
| dc.date.accessioned | 2026-07-07T08:26:05Z | |
| dc.date.available | 2026-07-07T08:26:05Z | |
| dc.description | 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. | |
| dc.identifier | https://arxiv.org/abs/0708.3721 | |
| dc.identifier | http://arxiv.org/abs/0708.3721 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/136825 | |
| dc.subject | Mathematical Software | |
| dc.subject | Logic in Computer Science | |
| dc.title | Verified Real Number Calculations: A Library for Interval Arithmetic | |
| dc.type | text |