已验证的实数计算：一个区间算术库
数学软件
2007-08-29 v1 计算机科学中的逻辑
摘要
在机械证明中处理初等函数的实数计算异常困难。在本文中，我们展示了如何在定理证明器或证明助手中，以便捷、高度自动化且交互式的方式执行这些计算。首先，我们形式化地建立了初等函数的上下界。然后，基于这些界，我们开发了一种有理区间算术，使实数计算在代数环境中进行。为了减小区间算术的依赖效应，我们整合了两种技术：区间分裂和 Taylor 级数展开。这种实用主义方法已在定理证明器中开发并得到形式化验证。形式化开发还包括一组可定制的策略，以自动化涉及实数显式计算的证明。我们的最终目标是提供具有最少人机交互的数值属性保证证明。
引用
@article{arxiv.0708.3721,
title = {Verified Real Number Calculations: A Library for Interval Arithmetic},
author = {Marc Daumas and David Lester and César Muñoz},
journal= {arXiv preprint arXiv:0708.3721},
year = {2007}
}