Ebook: Theorem Proving with the Real Numbers

This book discusses the use of the real numbers in theorem proving. Typ­ ically, theorem provers only support a few 'discrete' datatypes such as the natural numbers. However the availability of the real numbers opens up many interesting and important application areas, such as the verification of float­ ing point hardware and hybrid systems. It also allows the formalization of many more branches of classical mathematics, which is particularly relevant for attempts to inject more rigour into computer algebra systems. Our work is conducted in a version of the HOL theorem prover. We de­ scribe the rigorous definitional construction of the real numbers, using a new version of Cantor's method, and the formalization of a significant portion of real analysis. We also describe an advanced derived decision procedure for the 'Tarski subset' of real algebra as well as some more modest but practically useful tools for automating explicit calculations and routine linear arithmetic reasoning. Finally, we consider in more detail two interesting application areas. We discuss the desirability of combining the rigour of theorem provers with the power and convenience of computer algebra systems, and explain a method we have used in practice to achieve this. We then move on to the verification of floating point hardware. After a careful discussion of possible correctness specifications, we report on two case studies, one involving a transcendental function.

---

The Distinguished Dissertation series is published on behalf of the Conference of Professors and Heads of Computing and the British Computer Society, who annually select the best British PhD dissertations in computer science for publication. The dissertations are selected on behalf of the CPHC by a panel of eight academics. Each dissertation chosen makes a noteworthy contribution to the subject and reaches a high standard of exposition, placing all results clearly in the context of computer science as a whole. In this way computer scientists with significantly different interests are able to grasp the essentials - or even find a means of entry - to an unfamiliar research topic. Theorem Provingwith the Real Numbers discusses the formal development of classical mathematics using a computer. It combines traditional lines of research in theorem proving and computer algebra and shows the usefulness of real numbers in verification.

---

The Distinguished Dissertation series is published on behalf of the Conference of Professors and Heads of Computing and the British Computer Society, who annually select the best British PhD dissertations in computer science for publication. The dissertations are selected on behalf of the CPHC by a panel of eight academics. Each dissertation chosen makes a noteworthy contribution to the subject and reaches a high standard of exposition, placing all results clearly in the context of computer science as a whole. In this way computer scientists with significantly different interests are able to grasp the essentials - or even find a means of entry - to an unfamiliar research topic. Theorem Provingwith the Real Numbers discusses the formal development of classical mathematics using a computer. It combines traditional lines of research in theorem proving and computer algebra and shows the usefulness of real numbers in verification.
Content:
Front Matter....Pages i-xii
Introduction....Pages 1-11
Constructing the Real Numbers....Pages 13-38
Formalized Analysis....Pages 39-67
Explicit Calculations....Pages 69-86
A Decision Procedure for Real Algebra....Pages 87-114
Computer Algebra Systems....Pages 115-133
Floating Point Verification....Pages 135-154
Conclusions....Pages 155-159
Back Matter....Pages 161-186

---

The Distinguished Dissertation series is published on behalf of the Conference of Professors and Heads of Computing and the British Computer Society, who annually select the best British PhD dissertations in computer science for publication. The dissertations are selected on behalf of the CPHC by a panel of eight academics. Each dissertation chosen makes a noteworthy contribution to the subject and reaches a high standard of exposition, placing all results clearly in the context of computer science as a whole. In this way computer scientists with significantly different interests are able to grasp the essentials - or even find a means of entry - to an unfamiliar research topic. Theorem Provingwith the Real Numbers discusses the formal development of classical mathematics using a computer. It combines traditional lines of research in theorem proving and computer algebra and shows the usefulness of real numbers in verification.
Content:
Front Matter....Pages i-xii
Introduction....Pages 1-11
Constructing the Real Numbers....Pages 13-38
Formalized Analysis....Pages 39-67
Explicit Calculations....Pages 69-86
A Decision Procedure for Real Algebra....Pages 87-114
Computer Algebra Systems....Pages 115-133
Floating Point Verification....Pages 135-154
Conclusions....Pages 155-159
Back Matter....Pages 161-186
....