Formalization of real analysis: a survey of proof assistants and libraries †
Formalization of real analysis: a survey of proof assistants and libraries †
复制标题
DOI：
10.1017/s0960129514000437
复制
发表时间：
2015-01
影响因子：
0.5
通讯作者：
S. Boldo;Catherine Lelay;G. Melquiond
中科院分区：
文献类型：
--
作者：
S. Boldo;Catherine Lelay;G. Melquiond
近年来，许多证明系统已经改进到足以用于正式验证非平凡的数学结果。然而，它们有不同的目的，而且选择哪一个适合进行形式化工作并不总是容易的。在这篇文章中，我们重点讨论了与实分析有关的性质：实数、算术算子、极限、可微性、可积性等。我们选择研究以下系统在标准中提供的形式化：Coq， HOL4, HOL Light, Isabelle/HOL, Mizar， ProofPower-HOL和pv。我们还考虑了发挥类似作用或扩展标准库的大型开发：ACL2(r)用于ACL2， C-CoRN/MathClasses用于Coq，以及NASA PVS库。这个调查展示了实数在这些不同的证明中是如何被定义的，以及上面描述的实数分析的概念是如何被形式化的。我们还研究了这些系统为实际分析提供的自动化方法。
In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle/HOL, Mizar, ProofPower-HOL, and PVS. We have also accounted for large developments that play a similar role or extend standard libraries: ACL2(r) for ACL2, C-CoRN/MathClasses for Coq, and the NASA PVS library. This survey presents how real numbers have been defined in these various provers and how the notions of real analysis described above have been formalized. We also look at the methods of automation these systems provide for real analysis.