scientific article; zbMATH DE number 1303336

zbMATH Open0924.03022MaRDI QIDQ4249889FDOQ4249889

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)

• A system for automated deduction in engineering mechanics
• Title not available (Why is no real title available?)
• Title not available (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
• Title not available (Why is no real title available?)
• USING NONSTANDARD ANALYSIS TO ENSURE THE CORRECTNESS OF SYMBOLIC COMPUTATIONS
• Title not available (Why is no real title available?)

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)