Constructing the real numbers in HOL

DOI10.1007/BF01384233MaRDI QIDQ1334896zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

computer algebratheorem provingmathematical logic

Mathematics Subject Classification ID

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)

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

Cites work

• scientific article; zbMATH DE number 3118550 (Why is no real title available?)
• scientific article; zbMATH DE number 3165654 (Why is no real title available?)
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• scientific article; zbMATH DE number 3769599 (Why is no real title available?)
• scientific article; zbMATH DE number 107979 (Why is no real title available?)
• scientific article; zbMATH DE number 3506824 (Why is no real title available?)
• scientific article; zbMATH DE number 3521877 (Why is no real title available?)
• scientific article; zbMATH DE number 3548474 (Why is no real title available?)
• scientific article; zbMATH DE number 517013 (Why is no real title available?)
• scientific article; zbMATH DE number 3234211 (Why is no real title available?)
• scientific article; zbMATH DE number 3280240 (Why is no real title available?)
• scientific article; zbMATH DE number 3299973 (Why is no real title available?)
• scientific article; zbMATH DE number 3193050 (Why is no real title available?)
• scientific article; zbMATH DE number 3065102 (Why is no real title available?)
• A contribution to the theory of magnitudes and the foundations of analysis
• 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
• The Derivative a la Caratheodory
• The real numbers as a wreath product

Cited in

(16)

• scientific article; zbMATH DE number 1617296 (Why is no real title available?)
• A verified implementation of algebraic numbers in Isabelle/HOL
• Elements of mathematical analysis in PVS
• Error analysis of digital filters using HOL theorem proving
• The formalization of discrete Fourier transform in HOL
• Mechanizing Nonstandard Real Analysis
• scientific article; zbMATH DE number 1670741 (Why is no real title available?)
• scientific article; zbMATH DE number 1863376 (Why is no real title available?)
• Theory extension in ACL2(r)
• Survey article: The real numbers -- a survey of constructions
• Theorem Proving in Higher Order Logics
• Formalization of real analysis: a survey of proof assistants and libraries
• 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

Describes a project that uses

Uses Software

• HOL

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)