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 (18)
- 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
- Title not available (Why is that?)
- 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
- Algebraic Numbers in Isabelle/HOL
- Title not available (Why is that?)
- Certified Exact Transcendental Real Number Computation in Coq
- Classification of finite fields with applications
- Title not available (Why is that?)
- Title not available (Why is that?)
- A certifying square root and division elimination
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
- 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)
