Views of PI: Definition and computation
We study several formal proofs and algorithms related to the number pi in the context of Coq's standard library. In particular, we clarify the relation between roots of the cosine function and the limit of the alternated series whose terms are the inverse of odd natural numbers (known as Leibni...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2014-10-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | http://jfr.unibo.it/article/view/4343 |