Name
Abstract | ||
|---|---|---|
Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest scheme and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time this kind of mathematical proof is machine-checked. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-14052-5_12 | Clinical Orthopaedics and Related Research |
Keywords | DocType | Volume |
formal proof,mathematical pen-and-paper proof,asymptotic behavior,wave equation resolution scheme,main difficulty,comprehensive formalization,popular finite difference,numerical scheme,proper definition,mathematical proof,one-dimensional acoustic wave equation,method error,simplest scheme,partial differential equation,acoustic wave equation | Journal | abs/1001.4898 |
ISSN | ISBN | Citations |
Interactive Theorem Proving 6172 (2010) 147-162 | 3-642-14051-3 | 9 |
PageRank | References | Authors |
0.62 | 14 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sylvie Boldo | 1 | 292 | 26.85 |
| François Clément | 2 | 37 | 4.04 |
| Jean-Christophe Filliâtre | 3 | 615 | 45.86 |
| Micaela Mayero | 4 | 84 | 10.38 |
| Guillaume Melquiond | 5 | 345 | 24.82 |
| Pierre Weis | 6 | 151 | 19.20 |