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.9.1 Equality and ordering.- 2.9.2 Injecting the naturals.- 2.9.3 Addition.- 2.9.4 Multiplication.- 2.9.5 Completeness.- 2.9.6 Multiplicative inverse.- 2.10 Adding negative numbers.- 2.11 Handling equivalence classes.- 2.11.1 Defining a quotient type.- 2.11.2 Lifting operations.- 2.11.3 Lifting theorems.- 2.12 Summary and related work.- 3. Formalized Analysis.- 3.1 The rigorization and formalization of analysis.- 3.2 Some general theories.- 3.2.1 Metric spaces and topologies.- 3.2.2 Convergence nets.- 3.3 Sequences and series.- 3.3.1 Sequences.- 3.3.2 Series.- 3.4 Limits, continuity and differentiation.- 3.4.1 Proof by bisection.- 3.4.2 Some elementary analysis.- 3.4.3 The Caratheodory derivative.- 3.5 Power series and the transcendental functions.- 3.6 Integration.- 3.6.1 The Newton integral.- 3.6.2 The Riemann integral.- 3.6.3 The Lebesgue integral.- 3.6.4 Other integrals.- 3.6.5 The Kurzweil-Henstock gauge integral.- 3.6.6 Formalization in HOL.- 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.5.1 Integers.- 4.5.2 Negation.- 4.5.3 Absolute value.- 4.5.4 Addition.- 4.5.5 Subtraction.- 4.5.6 Multiplication by an integer.- 4.5.7 Division by an integer.- 4.5.8 Finite summations.- 4.5.9 Multiplicative inverse.- 4.5.10 Multiplication of real numbers.- 4.5.11 Thanscendental functions.- 4.5.12 Comparisons.- 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.3.1 Preliminary simplification.- 5.3.2 Reduction in context.- 5.3.3 Degree reduction.- 5.3.4 The main part of the algorithm.- 5.3.5 Reduction of formulas without an equation.- 5.3.6 Reduction of formulas with an equation.- 5.3.7 Reduction of intermediate formulas.- 5.3.8 Proof of termination.- 5.3.9 Comparison with Kreisel and Krivine.- 5.4 The HOL Implementation.- 5.4.1 Polynomial arithmetic.- 5.4.2 Encoding of logical properties.- 5.4.3 HOL versions of reduction theorems.- 5.4.4 Overall arrangement.- 5.5 Optimizing the linear case.- 5.5.1 Presburger arithmetic.- 5.5.2 The universal 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.2.1 Relevance to our topic.- 6.2.2 Relationship to NP problems.- 6.2.3 What must be internalized?.- 6.3 Combining systems.- 6.3.1 Thust.- 6.3.2 Implementation issues.- 6.4 Applications.- 6.4.1 Polynomial operations.- 6.4.2 Differentiation.- 6.4.3 Integration.- 6.4.4 Other examples.- 6.5 Summary and related work.- 7. Floating Point Verification.- 7.1 Motivation.- 7.1.1 Comprehensible specifications.- 7.1.2 Mathematical infrastructure.- 7.2 Floating point error analysis.- 7.3 Specifying floating point operations.- 7.3.1 Round to nearest.- 7.3.2 Bounded relative error.- 7.3.3 Error commensurate with likely input error.- 7.4 Idealized integer and floating point operations.- 7.5 A square root algorithm.- 7.6 A CORDIC 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 Computer algebra systems.- 8.5 Verification applications.- 8.6 Concluding remarks.- A. Logical foundations of HOL.- B. Recent developments.