A formal quantifier elimination for algebraically closed fields

Cyril Cohen 1, 2, 3, * Assia Mahboubi 1, 2, 3, *
* Corresponding author
1 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/inria-00464237
Contributor : Cyril Cohen <>
Submitted on : Monday, March 29, 2010 - 5:56:24 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on : Wednesday, November 30, 2016 - 4:35:29 PM

File

main.pdf
Files produced by the author(s)

Identifiers

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. pp.189-203, ⟨10.1007/978-3-642-14128-7_17⟩. ⟨inria-00464237v3⟩

Share

Metrics

Record views

639

Files downloads

967