Coq 中经认证的精确超越实数计算
计算机科学中的逻辑
2010-08-04 v1 数学软件
数值分析
摘要
在证明助手中对实数表达式进行推理具有挑战性。若干定理证明问题可通过使用精确实数计算得以解决。我在 Coq 证明助手中实现了一个用于推理和计算完备度量空间的库，并利用该库构建了包含基本实数函数及其正确性证明的构造性实数实现。借助该库，我创建了一种策略，可通过计算自动证明闭基本实数表达式上的严格不等式。
引用
@article{arxiv.0805.2438,
title = {Certified Exact Transcendental Real Number Computation in Coq},
author = {Russell O'Connor},
journal= {arXiv preprint arXiv:0805.2438},
year = {2010}
}
备注
This paper is to be part of the proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008)