Verified Real Number Calculations: A Library for Interval Arithmetic
Verified Real Number Calculations: A Library for Interval Arithmetic
复制标题
经验证的实数计算：区间算术库
DOI：
--
复制
发表时间：
2007
影响因子：
3.7
通讯作者：
C. Muñoz
中科院分区：
文献类型：
--
作者：
M. Daumas;D. Lester;C. Muñoz
初等函数的真实的数计算在机械证明中是非常困难的。在本文中，我们将展示如何在定理证明器或证明助手中以方便，高度自动化和交互式的方式执行这些计算。首先，我们正式建立了初等函数的上界和下界。然后，基于这些界限，我们开发了一个合理的区间算术的真实的数计算发生在一个代数设置。为了减少区间运算的依赖性，我们结合了两种技术：区间分裂和泰勒级数展开。这种实用的方法已经在定理证明器中开发并正式验证。正式的开发还包括一组可定制的策略，以自动化涉及真实的数字的显式计算的证明。我们的最终目标是提供有保证的数值性质的证明与最小的人类定理证明者的相互作用。
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.