Verification methods: rigorous results using floating-point arithmetic

Publikationstyp
Journal Article
Date Issued
2010-05-10
Sprache
English
Author(s)
Rump, Siegfried M.  orcid-logo
Institut
Zuverlässiges Rechnen E-19  
TORE-URI
http://hdl.handle.net/11420/8540
Journal
Acta numerica  
Volume
19
Start Page
287
End Page
449
Citation
Acta Numerica (19): 287-449 (2010-05-10)
Publisher DOI
10.1017/S096249291000005X
Scopus ID
2-s2.0-78149235132
Publisher
Cambridge Univ. Press
A classical mathematical proof is constructed using pencil and paper. However, there are many ways in which computers may be used in a mathematical proof. But proof by computer, or even the use of computers in the course of a proof, is not so readily accepted (the December 2008 issue of the Notices of the American Mathematical Society is devoted to formal proofs by computer). In the following we introduce verification methods and discuss how they can assist in achieving a mathematically rigorous result. In particular we emphasize how floating-point arithmetic is used.
DDC Class
004: Informatik