Name
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.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1145/3326229.3326240 | Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation |
Keywords | Field | DocType |
asymptotics, interactive theorem proving, isabelle, proof assistant, real analysis, symbolic computation | HOL,Discrete mathematics,Computer science,Correctness,Symbolic computation,Real analysis,Automation,Software,Mathematical proof,Calculus,Proof assistant | Conference |
ISBN | Citations | PageRank |
978-1-4503-6084-5 | 0 | 0.34 |
References | Authors | |
0 | 1 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Manuel Eberl | 1 | 11 | 13.27 |