## Abstract

The theorem prover Isabelle is used to formalise 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.

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.

Original language | English |
---|---|

Title of host publication | Automated Deduction — CADE-15 |

Subtitle of host publication | 15th International Conference on Automated Deduction Lindau, Germany, July 5–10, 1998 Proceedings |

Editors | Claude Kirchner, Hélène Kirchner |

Place of Publication | Berlin, Heidelberg |

Publisher | Springer Berlin Heidelberg |

Pages | 3-16 |

Number of pages | 14 |

ISBN (Electronic) | 978-3-540-69110-5 |

ISBN (Print) | 978-3-540-64675-4 |

DOIs | |

Publication status | Published - 1998 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Berlin Heidelberg |

Volume | 1421 |

ISSN (Print) | 0302-9743 |