Construction of real algebraic numbers in Coq
From MaRDI portal
Publication:2914733
DOI10.1007/978-3-642-32347-8_6zbMATH Open1360.68744OpenAlexW2134124371MaRDI QIDQ2914733FDOQ2914733
Authors: Cyril Cohen 
Publication date: 20 September 2012
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-32347-8_6
Recommendations
Cited In (19)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- A formalization of Dedekind domains and class groups of global fields
- Flexible proof production in an industrial-strength SMT solver
- Algebraic numbers in Isabelle/HOL
- A verified implementation of algebraic numbers in Isabelle/HOL
- Computing with classical real numbers
- Dealing with algebraic expressions over a field in Coq using Maple
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
- Certified Exact Transcendental Real Number Computation in Coq
- A formal proof of the irrationality of \(\zeta(3)\)
- Classification of finite fields with applications
- A simple canonical representation of rational numbers
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formalization techniques for asymptotic reasoning in classical analysis
- A certifying square root and division elimination
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- Constructing the real numbers in HOL
Uses Software
This page was built for publication: Construction of real algebraic numbers in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2914733)
