## A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's PrincipiaAbstract: "The theorem prover Isabelle is used to formalize and reproduce some of the styles of reasoning used by Newton in his Principia. The Principia's reasoning is resolutely geometric in nature but contains 'infinitesimal' elements and the presence of motion that take it beyond the traditional boundaries of Euclidean Geometry. These present difficulties that prevent Newton's proofs from being mechanised using only the existing geometry theorem proving (GTP) techniques. Using concepts from Robinson's Nonstandard Analysis (NSA) and a powerful geometric theory, we introduce the concept of an infinitesimal geometry in which quantities can be infinitely small or infinitesimal. We reveal and prove new properties of this geometry that only hold because infinitesimal elements are allowed and use them to prove lemmas and theorems from the Principia." |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Common terms and phrases

A B R A D AABR and AAD"R algebraic angle APPLICATION TO NEWTON'S arc.len area and full-angles area of SAB automated GTP Ballantyne and Bledsoe becomes infinitely close Bledsoe 12 Chou circular arc close to zero coll abc collinear COMBINATION OF NONSTANDARD complex mathematical content continuous motion curvilinear deduce diagram as point easily proved ellipse and tangents Equal Areas equivalence relation evanescent Fleuriot Lawrence follows formalisation in Isabelle full-angles methods geometric methods geometric proofs geometric properties geometric quantities Geometry Theorem Proving ideal in Finite impulsive centripetal force infinitely small infinitesimal from Nonstandard infinitesimal geometry Infmal introduce intuitive Kepler's Law Law of Equal len(A len(D manipulations of polynomials mechanised Newton's geometry Newton's Principia Newton's reasoning Nonstandard Analysis NSA numbers ordered field Pembroke Street Cambridge Point B moving proved in Isabelle S-delta Sd.it signed area straight edge tangent line techniques theory in Isabelle triangle SBC ultimately similar triangles University of Cambridge USIM