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…mehr
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 Proving with 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.
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.
Inhaltsangabe
- Introduction - Symbolic Computation - Verification - Higher Order Logic - Theorem Proving v Model Checking - Automated vs Interactive Theorem Proving - The Real Numbers - Concluding Remarks - Constructing the Real Numbers - Properties of the Real Numbers - Uniqueness of the Real Numbers - Constructing the Real Numbers - Positional Expansions - Cantor's Method - Dedekind's Method - What Choice?- Lemmas about Nearly-Multiplicative Functions - Details of the Construction - Adding Negative Numbers - Handling Equivalence Classes - Formalized Analysis - Explicit Calculations - A Decision Procedure for Real Algebra - Computer Algebra Systems - Floating Point Verification - Conclusions - Logical Foundations of HOL - Recent Developments.
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 Computer algebra systems.- 8.5 Verification applications.- 8.6 Concluding remarks.- A. Logical foundations of HOL.- B. Recent developments.
- Introduction - Symbolic Computation - Verification - Higher Order Logic - Theorem Proving v Model Checking - Automated vs Interactive Theorem Proving - The Real Numbers - Concluding Remarks - Constructing the Real Numbers - Properties of the Real Numbers - Uniqueness of the Real Numbers - Constructing the Real Numbers - Positional Expansions - Cantor's Method - Dedekind's Method - What Choice?- Lemmas about Nearly-Multiplicative Functions - Details of the Construction - Adding Negative Numbers - Handling Equivalence Classes - Formalized Analysis - Explicit Calculations - A Decision Procedure for Real Algebra - Computer Algebra Systems - Floating Point Verification - Conclusions - Logical Foundations of HOL - Recent Developments.
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 Computer algebra systems.- 8.5 Verification applications.- 8.6 Concluding remarks.- A. Logical foundations of HOL.- B. Recent developments.
Es gelten unsere Allgemeinen Geschäftsbedingungen: www.buecher.de/agb
Impressum
www.buecher.de ist ein Shop der buecher.de GmbH & Co. KG Bürgermeister-Wegele-Str. 12, 86167 Augsburg Amtsgericht Augsburg HRA 13309
