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 to help to prove and certify more efficient quantifier elimination procedures on reals.


This page was last updated at 2014-12-01 03:52:16 +0100
This site is compiled with nanoc and hosted by Cr@ns

Warning: fopen(index.log): failed to open stream: Permission denied in /home/cohen/www/phd/summary/index.php on line 75

Warning: fwrite() expects parameter 1 to be resource, bool given in /home/cohen/www/phd/summary/index.php on line 76

Warning: Use of undefined constant REMOTE_HOST - assumed 'REMOTE_HOST' (this will throw an Error in a future version of PHP) in /home/cohen/www/phd/summary/index.php on line 77

Notice: Undefined index: REMOTE_HOST in /home/cohen/www/phd/summary/index.php on line 77

Warning: Use of undefined constant REMOTE_ADDR - assumed 'REMOTE_ADDR' (this will throw an Error in a future version of PHP) in /home/cohen/www/phd/summary/index.php on line 77

Warning: fwrite() expects parameter 1 to be resource, bool given in /home/cohen/www/phd/summary/index.php on line 77

Warning: fclose() expects parameter 1 to be resource, bool given in /home/cohen/www/phd/summary/index.php on line 78