Jacques Fleuriot
Springer London
2001e druk, 2001
9781852334666
A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton’s Principia
Specificaties
Gebonden, 140 blz.
|
Engels
Springer London |
2001e druk, 2001
ISBN13: 9781852334666
Rubricering
Onderdeel van serie
Distinguished Dissertations
Verwachte levertijd ongeveer 9 werkdagen
Samenvatting
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.
Specificaties
ISBN13:9781852334666
Taal:Engels
Bindwijze:gebonden
Aantal pagina's:140
Uitgever:Springer London
Druk:2001
Inhoudsopgave
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.