A formal quantifier elimination for algebraically closed fields

Cyril Cohen 1, 2, 3, * Assia Mahboubi 1, 2, 3, *
* Auteur correspondant
1 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 : We prove formally that the first order theory of algebraically closed fields enjoy quantifier elimination, and hence is decidable. This proof is organized in two modular parts. We first reify the first order theory of rings and prove that quantifier elimination leads to decidability. Then we implement an algorithm which constructs a quantifier free formula from any first order formula in the theory of ring. If the underlying ring is in fact an algebraically closed field, we prove that the two formulas have the same semantic. The algorithm producing the quantifier free formula is programmed in continuation passing style, which leads to both a concise program and an elegant proof of semantic correctness.
Type de document :
Communication dans un congrès
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.189-203, 2010, Computer Science. 〈10.1007/978-3-642-14128-7_17〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00464237
Contributeur : Cyril Cohen <>
Soumis le : lundi 29 mars 2010 - 17:56:24
Dernière modification le : jeudi 9 février 2017 - 15:13:06
Document(s) archivé(s) le : mercredi 30 novembre 2016 - 16:35:29

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Cyril Cohen, Assia Mahboubi. A formal quantifier elimination for algebraically closed fields. Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.189-203, 2010, Computer Science. 〈10.1007/978-3-642-14128-7_17〉. 〈inria-00464237v3〉

Partager

Métriques

Consultations de
la notice

426

Téléchargements du document

620