Construction of real algebraic numbers in Coq

DOI10.1007/978-3-642-32347-8_6MaRDI QIDQ2914733zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Algebraic number theory computations (11Y40)

Recommendations

• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• scientific article; zbMATH DE number 2085168
• A verified implementation of algebraic numbers in Isabelle/HOL
• scientific article; zbMATH DE number 1263362
• scientific article; zbMATH DE number 1696612

Cited in

(19)

• A simple canonical representation of rational numbers
• Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
• A certifying square root and division elimination
• scientific article; zbMATH DE number 2085168 (Why is no real title available?)
• Algebraic numbers in Isabelle/HOL
• Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• Computing with classical real numbers
• A verified implementation of algebraic numbers in Isabelle/HOL
• Formalization techniques for asymptotic reasoning in classical analysis
• Certified Exact Transcendental Real Number Computation in Coq
• A formal proof of the irrationality of \(\zeta(3)\)
• Constructing the real numbers in HOL
• A formalization of Dedekind domains and class groups of global fields
• Flexible proof production in an industrial-strength SMT solver
• Dealing with algebraic expressions over a field in Coq using Maple
• scientific article; zbMATH DE number 1863376 (Why is no real title available?)
• Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
• Classification of finite fields with applications

Describes a project that uses

Uses Software

• Coq

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)