A library of Taylor models for PVS automatic proof checker

Francisco Cháves 1 Marc Daumas 1
1 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : We present in this report a library to compute with Taylor models, a technique extending interval arithmetic to reduce decorrelation and to solve differential equations. Numerical software usually produces only numerical results. Our library can be used to produce both results and proofs. As seen during the development of Fermat's last theorem reported by Acz96, providing a proof is not sufficient. Our library provides a proof that has been thoroughly scrutinized by a trustworthy and tireless assistant. PVS is an automatic proof assistant that has been fairly developed and used and that has no internal connection with interval arithmetic or Taylor models. We built our library so that PVS validates each result as it is produced. As producing and validating a proof, is and will certainly remain a bigger task than just producing a numerical result our library will never be a replacement to imperative implementations of Taylor models such as Cosy Infinity. Our library should mainly be used to validate small to medium size results that are involved in safety or life critical applications.
Document type :
Reports
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00070194
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 7:27:17 PM
Last modification on : Thursday, February 7, 2019 - 4:33:09 PM
Long-term archiving on : Sunday, April 4, 2010 - 8:30:49 PM

Identifiers

  • HAL Id : inria-00070194, version 1

Collections

Citation

Francisco Cháves, Marc Daumas. A library of Taylor models for PVS automatic proof checker. [Research Report] RR-5831, INRIA. 2006, pp.18. ⟨inria-00070194⟩

Share

Metrics

Record views

135

Files downloads

181