Constructing the real numbers in HOL
DOI10.1007/BF01384233zbMATH Open0809.68102OpenAlexW2022261955MaRDI QIDQ1334896FDOQ1334896
Authors: V. Pereyra 
Publication date: 26 September 1994
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf01384233
Recommendations
- A natural construction for the real numbers
- Generalized real numbers in constructive mathematics
- scientific article; zbMATH DE number 6736267
- scientific article; zbMATH DE number 517013
- Construction of the system of real numbers
- Two concrete new constructions of the real numbers
- Constructive analysis, types and exact real numbers
- scientific article; zbMATH DE number 2085165
- Construction of real algebraic numbers in Coq
Symbolic computation and algebraic computation (68W30) Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35) Foundations: limits and generalizations, elementary topology of the line (26A03)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The real numbers as a wreath product
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A contribution to the theory of magnitudes and the foundations of analysis
- Title not available (Why is that?)
- Implementing constructive real analysis (preliminary report)
- On the rate of convergence in the central limit theorem for sequences of weakly dependent, Hilbert-valued random variables
- Title not available (Why is that?)
- The Derivative a la Caratheodory
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (16)
- Title not available (Why is that?)
- Elements of mathematical analysis in PVS
- A verified implementation of algebraic numbers in Isabelle/HOL
- Error analysis of digital filters using HOL theorem proving
- The formalization of discrete Fourier transform in HOL
- Mechanizing Nonstandard Real Analysis
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theory extension in ACL2(r)
- Theorem Proving in Higher Order Logics
- Formalization of real analysis: a survey of proof assistants and libraries
- Survey article: The real numbers -- a survey of constructions
- Nonstandard analysis in ACL2
- Notes from the logbook of a proof-checker's project
- Formalization of fixed-point arithmetic in HOL
- Coquelicot: a user-friendly library of real analysis for Coq
Uses Software
This page was built for publication: Constructing the real numbers in HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1334896)
