A formal quantifier elimination for algebraically closed fields
A formal quantifier elimination for algebraically closed fields
复制标题
DOI：
10.1007/978-3-642-14128-7_17
复制
发表时间：
2010-07
期刊：
影响因子：
--
通讯作者：
C. Cohen;A. Mahboubi
中科院分区：
文献类型：
--
作者：
C. Cohen;A. Mahboubi
我们正式证明代数闭域的一阶理论具有量词消除，因此是可判定的。该证明由两个模块部分组成。我们首先具体化环的一阶理论并证明量词消除导致可判定性。然后我们实现一种算法，从环理论中的任何一阶公式构造一个无量词公式。如果底层环实际上是一个代数闭域，我们证明这两个公式具有相同的语义。生成无量词公式的算法以连续传递风格进行编程，这既产生了简洁的程序，又提供了语义正确性的优雅证明。
We prove formally that the first order theory of algebraically closed fields enjoys 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.