Overview

Sir Isaac Newton's philosophi Naturalis Principia Mathematica'(the Principia) contains a prose-style mixture of geometric and limit reasoning that has often been viewed as logically vague. In A Combination of Geometry Theorem Proving and Nonstandard Analysis, Jacques Fleuriot presents a formalization of Lemmas and Propositions from the Principia using a combination of methods from geometry and nonstandard analysis. The mechanization of the procedures, which respects much of Newton's original reasoning, is developed within the theorem prover Isabelle. The application of this framework to the mechanization of elementary real analysis using nonstandard techniques is also discussed.

Full Product Details

Author:   Jacques Fleuriot
Publisher:   Springer London Ltd
Imprint:   Springer London Ltd
Edition:   Softcover reprint of the original 1st ed. 2001
Dimensions:   Width: 15.50cm , Height: 0.80cm , Length: 23.50cm
Weight:   0.256kg
ISBN:  

9781447110415

ISBN 10:   1447110412
Pages:   140
Publication Date:   13 September 2012
Audience:   Professional and scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   Manufactured on demand  
We will order this item for you from a manufactured on demand supplier.

Table of Contents

1. Introduction.- 1.1 A Brief History of th e Infinitesimal.- 1.2 The Principia and its Methods.- 1.3 On Nonstandard Analysis.- 1.4 Objectives.- 1.5 Achieving our Goals.- 1.6 Organisation of this Book.- 2. Geometry Theorem Proving.- 2.1 Historical Background.- 2.2 Algebraic Techniques.- 2.3 Coordinate-Free Techniques.- 2.4 Formalizing Geometry in Isabelle.- 2.5 Concluding Remarks.- 3. Constructing the Hyperreals.- 3.1 Isabelle/HOL.- 3.2 Propertiesof an Infinitesimal Calculus.- 3.3 Internal Set Theory.- 3.4 Constructions Leading to the Reals.- 3.5 Filters and Ultrafilters.- 3.6 Ultrapower Construction of the Hyperreals.- 3.7 Structure of the Hyperreal Number Line.- 3.8 The Hypernatural Numbers.- 3.9 An Alternative Construction for the Reals.- 3.10 Related Work.- 3.11 Concluding Remarks.- 4. Infinitesimal and Analytic Geometry.- 4.1 Non-Archimedean Geometry.- 4.2 New Definitions and Relations.- 4.3 Infinitesimal Geometry Proofs.- 4.4 Verifying the Axioms of Geometry.- 4.5 Concluding Remarks.- 5. Mechanizing Newton’s Principia.- 5.1 Formalizing Newton’s Properties.- 5.2 Mechanized Propositions and Lemmas.- 5.3 Ratios of Infinitesimals.- 5.4 Case Study : Propositio Kepleriana.- 6. Nonstandard Real Analysis.- 6.1 Extending a Relation to the Hyperreals.- 6.2 Towards an Intuitive Calculus.- 6.3 Real Sequences and Series.- 6.4 Some Elementary Topology of the Reals.- 6.5 Limits and Continuity.- 6.6 Differentiation.- 6.7 On the Transfer Principle.- 6.8 Related Work and Conclusions.- 7. Conclusions.- 7.1 Geometry, Newton , and the Principia.- 7.2 Hyperreal Analysis.- 7.3 Further Work.- 7.4 Concluding Remarks.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions