Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

Cyril Cohen 1, 2, 3 Assia Mahboubi 4, 1, 2, 3
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic properties. The theory of real algebraic numbers and more generally of semi-algebraic varieties is at the core of a number of effective methods in real analysis, including decision procedures for non linear arithmetic or optimization methods for real valued functions. After defining an abstract structure of discrete real closed field and the elementary theory of real roots of polynomials, we describe the formalization of an algebraic proof of quantifier elimination based on pseudo-remainder sequences following the standard computer algebra literature on the topic. This formalization covers a large part of the theory which underlies the efficient algorithms implemented in practice in computer algebra. The success of this work paves the way for formal certification of these efficient methods.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. <10.2168/LMCS-8 (1:02) 2012>
Liste complète des métadonnées


https://hal.inria.fr/inria-00593738
Contributeur : Cyril Cohen <>
Soumis le : jeudi 16 février 2012 - 14:19:27
Dernière modification le : jeudi 9 février 2017 - 15:11:36
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 06:20:07

Fichier

1201.3731.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Cyril Cohen, Assia Mahboubi. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. <10.2168/LMCS-8 (1:02) 2012>. <inria-00593738v4>

Partager

Métriques

Consultations de
la notice

652

Téléchargements du document

748