Formalized algebraic numbers: construction and first-order theory.

Abstract : This thesis presents a formalization of algebraic numbers and their theory. It brings two new important contributions to the formalization of mathematical results in proof assistants, Coq in our case: the intuitionistic construction of real algebraic numbers together with the proof they form a real closed field, and the programming and certification of quantifier elimination procedures for the theories of algebraically closed fields and real closed fields. In order to reach those results, we brought multiple contributions to the toolboxes and formalization and proof methodologies in Coq. More particularly, we provide in Coq/SSReflect a framework to work with quotient types. We provide a complete library about ordered and normed number algebraic structures. We wrote a short implementation of Cauchy reals together with tactics to deal easily with reasoning using assertions of the form "let n be a big enough number", commonly used in mathematical paper proofs. We also developed a short library of real polynomial analysis. A big part of our contributions is useful for the formalization of the proof of Odd Order Theorem and they also aim at helping to prove and certify more efficient quantifier elimination procedures on reals.
Complete list of metadatas

Cited literature [86 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00780446
Contributor : Cyril Cohen <>
Submitted on : Thursday, January 24, 2013 - 3:30:41 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on : Saturday, April 1, 2017 - 9:46:21 AM

File

Identifiers

  • HAL Id : pastel-00780446, version 1

Collections

Citation

Cyril Cohen. Formalized algebraic numbers: construction and first-order theory.. Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English. ⟨pastel-00780446⟩

Share

Metrics

Record views

789

Files downloads

1137