scientific article; zbMATH DE number 1646230

MaRDI QIDQ2739733zbMATH OpenFDO

Authors Jacques D. Fleuriot

Publication date 16 September 2001

Published in Distinguished Dissertations (Search for Journal in Brave)

zbMATH Keywords

geometry theorem provingNewton's Principianonstandard analysistheorem prover Isabelle

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Recommendations

• A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia
• USING NONSTANDARD ANALYSIS TO ENSURE THE CORRECTNESS OF SYMBOLIC COMPUTATIONS
• Proving Newton's Propositio Kepleriana using geometry and nonstandard analysis in Isabelle
• scientific article; zbMATH DE number 4201687
• scientific article; zbMATH DE number 1746669

Cited in

(14)

• Mechanised modal model theory
• Non-standard analysis in dynamic geometry
• Theorem proving in infinitesimal geometry
• Exploring the foundations of discrete analytical geometry in Isabelle/HOL
• scientific article; zbMATH DE number 6828421 (Why is no real title available?)
• A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia
• Mechanizing Nonstandard Real Analysis
• scientific article; zbMATH DE number 1746669 (Why is no real title available?)
• Computational logic: its origins and applications
• Proving Newton's Propositio Kepleriana using geometry and nonstandard analysis in Isabelle
• What is a proof?
• Formalization of gyrovector spaces as models of hyperbolic geometry and special relativity
• Simultaneous orthogonalization of inner products in infinite-dimensional vector spaces
• A proof-centric approach to mathematical assistants

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 Q2739733)