scientific article; zbMATH DE number 1303336

MaRDI QIDQ4249889zbMATH OpenFDO

Authors Jacques D. Fleuriot, Lawrence C. Paulson

Publication date 16 November 1999

zbMATH Keywords

geometry theorem provingNonstandard AnalysisNewton's Principiainfinitesimal geometrytheorem prover Isabelle

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Nonstandard models in mathematics (03H05) Nonstandard analysis (26E35) Software, source code, etc. for problems pertaining to real functions (26-04)

Recommendations

• scientific article; zbMATH DE number 1646230
• Theorem proving in infinitesimal geometry
• scientific article; zbMATH DE number 1746669
• Publication:4946078

Cited in

(9)

• scientific article; zbMATH DE number 6828421 (Why is no real title available?)
• A system for automated deduction in engineering mechanics
• scientific article; zbMATH DE number 1646230 (Why is no real title available?)
• scientific article; zbMATH DE number 1746669 (Why is no real title available?)
• Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
• Exploring the foundations of discrete analytical geometry in Isabelle/HOL
• Theorem proving in infinitesimal geometry
• scientific article; zbMATH DE number 1421054 (Why is no real title available?)
• USING NONSTANDARD ANALYSIS TO ENSURE THE CORRECTNESS OF SYMBOLIC COMPUTATIONS

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