scientific article; zbMATH DE number 1421054

MaRDI QIDQ4946078zbMATH OpenFDO

Authors Jacques D. Fleuriot, Lawrence C. Paulson

Publication date 11 January 2001

zbMATH Keywords

geometry theorem provingNonstandard AnalysisPropositio Keplerianatheorem prover Isabelle

Mathematics Subject Classification ID

History of mathematics in the 17th century (01A45) Mechanization of proofs and logical operations (03B35) Nonstandard models in mathematics (03H05) Nonstandard analysis (26E35) Software, source code, etc. for problems pertaining to mechanics of particles and systems (70-04) Celestial mechanics (70F15)

Recommendations

• scientific article; zbMATH DE number 1646230
• scientific article; zbMATH DE number 1303336
• Newton's \textit{Principia} and inverse-square orbits: The flaw reexamined
• Kepler's area law in the \textit{Principia}: filling in some details in Newton's proof of Proposition 1.
• Newton's mature dynamics and the Principia: A simplified solution to the Kepler problem

Cited in

(4)

• scientific article; zbMATH DE number 1646230 (Why is no real title available?)
• Exploring the foundations of discrete analytical geometry in Isabelle/HOL
• scientific article; zbMATH DE number 1303336 (Why is no real title available?)
• Automated theorem provers: a practical tool for the working mathematician?

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4946078)