Theorem proving in infinitesimal geometry

DOI10.1093/JIGPAL/9.3.447MaRDI QIDQ2720298zbMATH OpenOpenAlexFDO

Authors Jacques D. Fleuriot

Publication date 26 June 2001

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/9.3.447

zbMATH Keywords

algebraic geometry theoryhigher-order logichyperrealsinfinitesimal geometryIsabellenonstandard analysistheorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Nonstandard models in mathematics (03H05)

Recommendations

• scientific article; zbMATH DE number 1746669
• scientific article; zbMATH DE number 1303336
• scientific article; zbMATH DE number 1263333
• scientific article; zbMATH DE number 1646230
• Mechanizing Nonstandard Real Analysis

Cited in

(8)

• Formalization of the Poincaré disc model of hyperbolic geometry
• Formalizing complex plane geometry
• From informal to formal proofs in Euclidean geometry
• Exploring the foundations of discrete analytical geometry in Isabelle/HOL
• Formalizing Hilbert's Grundlagen in Isabelle/Isar
• scientific article; zbMATH DE number 1303336 (Why is no real title available?)
• Mechanizing Nonstandard Real Analysis
• scientific article; zbMATH DE number 1746669 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: Theorem proving in infinitesimal geometry

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