Theorem Proving with the Real Numbers

1. Introduction.- 1.1 Symbolic computation.- 1.2 Verification.- 1.3 Higher order logic.- 1.4 Theorem proving vs. model checking.- 1.5 Automated vs. interactive theorem proving.- 1.6 The real numbers.- 1.7 Concluding remarks.- 2 Constructing the Real Numbers.- 2.1 Properties of the real numbers.- 2.2 Uniqueness of the real numbers.- 2.3 Constructing the real numbers.- 2.4 Positional expansions.- 2.5 Cantor's method.- 2.6 Dedekind's method.- 2.7 What choice?.- 2.8 Lemmas about nearly-multiplicative functions.- 2.9 Details of the construction.- 2.10 Adding negative numbers.- 2.11 Handling equivalence classes.- 2.12 Summary and related work.- 3. Formalized Analysis.- 3.1 The rigorization and formalization of analysis.- 3.2 Some general theories.- 3.3 Sequences and series.- 3.4 Limits, continuity and differentiation.- 3.5 Power series and the transcendental functions.- 3.6 Integration.- 3.7 Summary and related work.- 4. Explicit Calculations.- 4.1 The need for calculation.- 4.2 Calculation with natural numbers.- 4.3 Calculation with integers.- 4.4 Calculation with rationals.- 4.5 Calculation with reals.- 4.6 Summary and related work.- 5. A Decision Procedure for Real Algebra.- 5.1 History and theory.- 5.2 Real closed fields.- 5.3 Abstract description of the algorithm.- 5.4 The HOL Implementation.- 5.5 Optimizing the linear case.- 5.6 Results.- 5.7 Summary and related work.- 6. Computer Algebra Systems.- 6.1 Theorem provers vs. computer algebra systems.- 6.2 Finding and checking.- 6.3 Combining systems.- 6.4 Applications.- 6.5 Summary and related work.- 7. Floating Point Verification.- 7.1 Motivation.- 7.2 Floating point error analysis.- 7.3 Specifying floating point operations.- 7.4 Idealized integer and floating point operations.- 7.5 A square root algorithm.- 7.6 ACORDIC natural logarithm algorithm.- 7.7 Summary and related work.- 8. Conclusions.- 8.1 Mathematical contributions.- 8.2 The formalization of mathematics.- 8.3 The LCF approach to theorem proving.- 8.4

John Harrison has had a lifelong interest in wildlife, and birds in particular. In 1973 he was appointed as a radio producer in the BBC Natural History Unit; during the 18 years he was there, he worked with most of the top naturalists and ornithologists in Britain. As a birdwatcher and wildlife enthusiast, he has made many visits to Sri Lanka over a number of years, and has a first-hand knowledge of the Sri Lankan avifauna. He is now the voluntary warden of a 70 ha wetland nature reserve for the Avon Wildlife Trust.