Construction of Real Algebraic Numbers in Coq
Construction of Real Algebraic Numbers in Coq
复制标题
在 Coq 中构建实代数数
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
C. Cohen
中科院分区：
文献类型：
--
作者：
C. Cohen
给出了实代数集在余q中的一种构造，并给出了它具有离散阿基米德实闭域结构的形式证明。因此，这种构造实现了一个真正的封闭场的接口。由于以前的工作，这样的接口的实例立即享受量词消除。这项工作也旨在成为构造复代数数的基础，并为计算机代数中依赖于代数数的众多算法的证明提供参考实现。
This paper shows a construction in Coq of the set of real algebraic numbers, together with a formal proof that this set has a structure of discrete Archimedean real closed field. This construction hence implements an interface of real closed field. Instances of such an interface immediately enjoy quantifier elimination thanks to a previous work. This work also intends to be a basis for the construction of complex algebraic numbers and to be a reference implementation for the certification of numerous algorithms relying on algebraic numbers in computer algebra.