Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle

Jacques D. Fleuriot, Lawrence C. Paulson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The approach previously used to mechanise lemmas and Kepler’s Law of Equal Areas from Newton’s Principia [13] is here used to mechanically reproduce the famous Propositio Kepleriana or Kepler Problem. This is one of the key results of the Principia in which Newton demonstrates that the centripetal force acting on a body moving in an ellipse obeys an inverse square law. As with the previous work, the mechanisation is carried out through a combination of techniques from geometry theorem proving (GTP) and Nonstandard Analysis (NSA) using the theorem prover Isabelle. This work demonstrates the challenge of reproducing mechanically Newton’s reasoning and how the combination of methods works together to reveal what we believe to be flaw in Newton’s reasoning.
Original languageEnglish
Title of host publicationAutomated Deduction in Geometry
Subtitle of host publicationSecond International Workshop, ADG’98 Beijing, China, August 1–3, 1998 Proceedings
EditorsXiao-Shan Gao, Dongming Wang, Lu Yang
PublisherSpringer Berlin Heidelberg
Pages47-66
Number of pages20
ISBN (Electronic)978-3-540-47997-0
ISBN (Print)978-3-540-66672-1
DOIs
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume1669
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle'. Together they form a unique fingerprint.

Cite this