Verified Real Asymptotics in Isabelle/HOL

DOI10.1145/3326229.3326240zbMath1467.68204OpenAlexW2957176605MaRDI QIDQ5120486

Manuel Eberl

Publication date: 10 September 2020

Published in: Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3326229.3326240

zbMATH Keywords

asymptoticssymbolic computationreal analysisproof assistantinteractive theorem provingIsabelle

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Foundations: limits and generalizations, elementary topology of the line (26A03) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Unnamed Item ⋮ Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL ⋮ Nine Chapters of Analytic Number Theory in Isabelle/HOL. ⋮ A Perron-Frobenius theorem for deciding matrix growth ⋮ Verified interactive computation of definite integrals

Uses Software

• Isabelle/HOL

This page was built for publication: Verified Real Asymptotics in Isabelle/HOL