Constructing the real numbers in HOL
type: Item
instance of: scholarly article
title: Constructing the real numbers in HOL
zbMATH Open document ID: 0809.68102
DOI: 10.1007/BF01384233
author: V. Pereyra
published in: Formal Methods in System Design
publication date: 1994-09-26T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 68W30
Mathematics Subject Classification ID: 26A03
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 644671
zbMATH Keywords: mathematical logic
zbMATH Keywords: theorem proving
zbMATH Keywords: computer algebra
describes a project that uses: HOL
MaRDI profile type: Publication
cites work: A contribution to the theory of magnitudes and the foundations of analysis
cites work: Q3803111
cites work: Q5522002
cites work: Q4087300
cites work: Q3283995
cites work: Q5581797
cites work: Q5565254
cites work: Implementing constructive real analysis (preliminary report)
cites work: Q5729383
cites work: Q4099541
cites work: The real numbers as a wreath product
cites work: Q4023553
cites work: Q4282537
cites work: On the rate of convergence in the central limit theorem for sequences of weakly dependent, Hilbert-valued random variables
cites work: Q4122841
cites work: The Derivative a la Caratheodory
cites work: Q5804274
cites work: Q3950538
cites work: Q3233328
full work available at URL: https://doi.org/10.1007/bf01384233
OpenAlex ID: W2022261955
Recommended article: A natural construction for the real numbers
Recommended article: Generalized real numbers in constructive mathematics
Recommended article: Q5269763
Recommended article: Q4282537
Recommended article: Construction of the system of real numbers
Recommended article: Two concrete new constructions of the real numbers
Recommended article: Constructive analysis, types and exact real numbers
Recommended article: Q4736388
Recommended article: Construction of Real Algebraic Numbers in Coq
description: scientific article; zbMATH DE number 644671