Mechanizing Nonstandard Real Analysis

DOI10.1112/S1461157000000267MaRDI QIDQ4504968zbMATH OpenOpenAlexWikidataFDO

Authors Jacques D. Fleuriot, Lawrence C. Paulson

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

filtershigher-order logichyperrealsinfinite numbersinfinitesimalsmechanical theorem-provingnonstandard analysistheorem-prover Isabelleultrafilters

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1670741
• Constructing the real numbers in HOL
• scientific article; zbMATH DE number 1646230
• A constructive approach to nonstandard analysis
• Theorem proving in infinitesimal geometry

Cites work

• A formulation of the simple theory of types
• Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques
• Free-variable axiomatic foundations of infinitesimal analysis: A fragment with finitary consistency proof
• scientific article; zbMATH DE number 3933369 (Why is no real title available?)
• scientific article; zbMATH DE number 3521877 (Why is no real title available?)
• scientific article; zbMATH DE number 3525429 (Why is no real title available?)
• scientific article; zbMATH DE number 1259143 (Why is no real title available?)
• scientific article; zbMATH DE number 1059780 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Infinitely small quantities in Cauchy's textbooks
• Isabelle. A generic theorem prover
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• USING NONSTANDARD ANALYSIS TO ENSURE THE CORRECTNESS OF SYMBOLIC COMPUTATIONS

Cited in

(14)

• The flow of ODEs: formalization of variational equation and Poincaré map
• Organizing numerical theories using axiomatic type classes
• Theory extension in ACL2(r)
• Theorem proving in infinitesimal geometry
• scientific article; zbMATH DE number 1670741 (Why is no real title available?)
• scientific article; zbMATH DE number 5932228 (Why is no real title available?)
• Banishing ultrafilters from our consciousness
• scientific article; zbMATH DE number 69482 (Why is no real title available?)
• scientific article; zbMATH DE number 1746669 (Why is no real title available?)
• USING NONSTANDARD ANALYSIS TO ENSURE THE CORRECTNESS OF SYMBOLIC COMPUTATIONS
• A Nonstandard Functional Programming Language
• Type classes and filters for mathematical analysis in Isabelle/HOL
• Nonstandard analysis in ACL2
• Equivalence of the traditional and non-standard definitions of concepts from real analysis

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: Mechanizing Nonstandard Real Analysis

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