inria-00464237, version 3
A formal quantifier elimination for algebraically closed fields
Cyril Cohen
a, 1, 2, 3Assia Mahboubi a, 1, 2, 3
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus 6167 (2010) 189-203
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.
- a – INRIA
- 1: TypiCal (INRIA Saclay - Ile de France)
- INRIA – CNRS : UMR – Polytechnique - X
- 2: Microsoft Research - Inria Joint Centre (MSR - INRIA)
- INRIA – Microsoft – Microsoft Research Laboratory Cambridge
- 3: Laboratoire d'informatique de l'école polytechnique (LIX)
- CNRS : UMR7161 – Polytechnique - X
- Domain : Computer Science/Logic in Computer Science
Computer Science/Symbolic Computation - Keywords : coq – quantifier elimination – closed fields – continuation passing style – algebra
- Comment : The final publication is available at www.springerlink.com
- Available versions : v1 (2010-03-16) v2 (2010-03-21) v3 (2010-03-30)
- inria-00464237, version 3
- http://hal.inria.fr/inria-00464237
- oai:hal.inria.fr:inria-00464237
- From: Cyril Cohen
- Submitted on: Monday, 29 March 2010 17:56:24
- Updated on: Tuesday, 14 September 2010 14:14:02
Associated documents
Export