Mechanizing Nonstandard Real Analysis

DOI10.1112/S1461157000000267zbMath0951.03006OpenAlexW1981484178WikidataQ57382694 ScholiaQ57382694MaRDI QIDQ4504968

Lawrence Charles Paulson, Jacques D. Fleuriot

Publication date: 25 September 2000

Published in: LMS Journal of Computation and Mathematics (Search for Journal in Brave)

Full work available at URL: http://www.lms.ac.uk/jcm/3/lms1999-027/

zbMATH Keywords

higher-order logicnonstandard analysisfiltersultrafiltershyperrealsinfinitesimalsinfinite numbersmechanical theorem-provingtheorem-prover Isabelle

Mathematics Subject Classification ID

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

Related Items (2)

The flow of ODEs: formalization of variational equation and Poincaré map ⋮ Organizing numerical theories using axiomatic type classes

Uses Software

• Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Infinitely small quantities in Cauchy's textbooks
• Isabelle. A generic theorem prover
• Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques
• Free-variable axiomatic foundations of infinitesimal analysis: A fragment with finitary consistency proof
• USING NONSTANDARD ANALYSIS TO ENSURE THE CORRECTNESS OF SYMBOLIC COMPUTATIONS
• A formulation of the simple theory of types
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice

This page was built for publication: Mechanizing Nonstandard Real Analysis