带二次幂谓词的实数理论的量子消除
计算机科学中的逻辑
2007-05-23 v1
摘要
1985 年，van den Dries 展示了实数理论中带整数二次幂谓词的量子消除在扩充语言中是可实现的，从而是可判定的。他给出的是一种模型论证方法，未能提供判决程序的复杂度界限。我们提供了一种语法证明方法，得到一个原始递归的程序，尽管其非初等。具体而言，我们证明可以在时间 上消除单个存在量子块，其中 为输入公式的长度， 表示 次迭代幂运算。
引用
@article{arxiv.cs/0610117,
title = {Quantifier elimination for the reals with a predicate for the powers of two},
author = {Jeremy Avigad and Yimu Yin},
journal= {arXiv preprint arXiv:cs/0610117},
year = {2007}
}