A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton's Principia / Edition 1

A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton's Principia / Edition 1

by Jacques Fleuriot
     
 

ISBN-10: 1852334665

ISBN-13: 9781852334666

Pub. Date: 10/25/2007

Publisher: Springer London

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

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.

Product Details

ISBN-13:
9781852334666
Publisher:
Springer London
Publication date:
10/25/2007
Series:
Distinguished Dissertations Series
Edition description:
2001
Pages:
140
Product dimensions:
0.44(w) x 9.21(h) x 6.14(d)

Table of Contents

Introduction.- A Brief History of the Infinitesimal.- The Principia and its Methods.- On Nonstandard Analysis.- Objectives.- Achieving our Goals.- Organisation of this book.- Geometry Theorem Proving.- Historical Background.- Algebraic Techniques.- Coordinate-Free Techniques.- Formalizing Geometry in Isabelle.- Concluding remarks.- Constructing the Hy perreals.- Isabelle/HOL.- Properties of an Infinitesimal Calculus.- Internal Set Theory.- Constructions Leading to the Reals.- Filters and Ultrafilters.- Ultrapower Construction of the Hyperreals.- Structure of the Hyperreal Number Line.- The Hypernatural Numbers.- An Alternative Construction for the Reals.- Related Work.- Concluding Remarks.- Infinitesimal and Analytic Geometry.- Non-Archimedean Geometry.- New Definitions and Relations.- Infinitesimal Geometry Proofs.- Verifying the Axioms of Geometry.- Concluding Remarks.- Mechanising Newton's Principia.- Formalizing Newton's Properties.- Mechanized Propositions and Lemmas.- Ratios of Infinitesimals.- Case Study: Propositio Kepleriana.- Expanding Newton's Proof.- Conclusions.- Nonstandard Real Analysis.- Extending a Relation to the Hyperreals.- Towards an Intuitive Calculus.- Real Sequences and Series.- Some Elementary Topology of the Reals.- Limits and Continuity.- Differentiation.- On the Transfer Principle.- Related Work and Conclusions.- Conclusions.- Geometry, Newton and the Principia.- Hyperreal Analysis.- Further Work.- Concluding Remarks.-

Customer Reviews

Average Review:

Write a Review

and post it to your social network

     

Most Helpful Customer Reviews

See all customer reviews >