Constructing the real numbers in HOL

DOI10.1007/BF01384233zbMath0809.68102OpenAlexW2022261955MaRDI QIDQ1334896

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

theorem provingcomputer algebramathematical 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)

Related Items

The formalization of discrete Fourier transform in HOL, Formalization of real analysis: a survey of proof assistants and libraries, Survey article: The real numbers -- a survey of constructions, Error analysis of digital filters using HOL theorem proving, Coquelicot: a user-friendly library of real analysis for Coq, Formalization of fixed-point arithmetic in HOL

Uses Software

• HOL

Cites Work

• A contribution to the theory of magnitudes and the foundations of analysis
• On the rate of convergence in the central limit theorem for sequences of weakly dependent, Hilbert-valued random variables
• The real numbers as a wreath product
• The Derivative a la Caratheodory
• Implementing constructive real analysis (preliminary report)
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item