Logic for exact real arithmetic

MaRDI QIDQ4989402zbMATH OpenFDO

Authors Helmut Schwichtenberg, Franziskus Wiesnet

Publication date 25 May 2021

Full work available at URL https://arxiv.org/abs/1904.12763, https://lmcs.episciences.org/7383

zbMATH Keywords

corecursioninductive and coinductive definitionsprogram extractionreal number computationrealizabilitysigned digit code

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Program extraction in exact real arithmetic
• From coinductive proofs to exact real arithmetic: theory and applications
• From Coinductive Proofs to Exact Real Arithmetic
• Logic for Exact Real Arithmetic: Multiplication
• Coinductive Formal Reasoning in Exact Real Arithmetic

Cites work

• A certified, corecursive implementation of exact real numbers
• An abstract data type for real numbers
• From Coinductive Proofs to Exact Real Arithmetic
• scientific article; zbMATH DE number 3664931 (Why is no real title available?)
• scientific article; zbMATH DE number 3687373 (Why is no real title available?)
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• scientific article; zbMATH DE number 3310901 (Why is no real title available?)
• Logic for Gray-code computation
• Program extraction in exact real arithmetic
• Proofs and computations
• Real number computation through Gray code embedding.
• Zur Deutung der intuitionistischen Logik

Cited in

(7)

• Exact real arithmetic for interval number systems
• Axiomatic reals and certified efficient exact real computation
• Lookahead analysis in exact real arithmetic with logical methods
• Limits of real numbers in the binary signed digit representation
• Logic for Exact Real Arithmetic: Multiplication
• Logic for exact real arithmetic
• Verified program extraction in number theory: the fundamental theorem of arithmetic and relatives

This page was built for publication: Logic for exact real arithmetic

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