Verified Real Asymptotics in Isabelle/HOL

by Manuel Eberl

In: Proceedings of ISSAC 2019

SIGSAM Distinguished Student Author Award

DOI:

Abstract:

Interactive theorem provers (or proof assistants) are software with which mathematical definitions and theorems can be formalised. They assist the user in writing formal proofs and check the correctness of these proofs, typically down to the level of basic logical inference steps. This provides a very high degree of assurance that any proof accepted by them is actually sound. Theorem provers contain varying amounts of tools for automation to assist the user, but unlike computer algebra systems, their focus is not on efficient automatic computation.

In this work, we focus on the particular problem of symbolically determining and proving asymptotics of real-valued functions: limits, ‘Big-O’ statements, and asymptotic expansions. The tool that is presented here uses an approach based on multiseries expansions and can handle functions built from basic arithmetic and standard functions like exp, ln, sin, |·|, etc. as well as parameters. The procedure is efficient enough to handle big problems and it is fully automatic in many cases.

Download preprint PDF (626 KiB)

@inproceedings{eberl19issac,
 author = "Eberl, Manuel",
 editor = "James H. Davenport and Dongming Wang and Manuel Kauers and Russell J. Bradford"
 title = "Verified Real Asymptotics in {I}sabelle/{HOL}",
 booktitle = "International Symposium on Symbolic and Algebraic Computation, {ISSAC} 2019",
 year = "2019",
 isbn = "978-1-4503-6084-5/19/07",
 doi = "10.1145/3326229.3326240",
 publisher = "ACM"
}

Download BibTeX (404 Bytes)

(The final publication is available at ACM)