<p>I'm looking for some formula/expression in a citable resource, that gives the running time for Tarski's quantifier elimination.</p>

<p>In my search, I only found the statement "it's not elementary" on several pages and papers.
But given the explanation on <a href="https://en.wikipedia.org/wiki/ELEMENTARY" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/ELEMENTARY</a>, this could allow for a "power tower" like <span class="math-container">$\exp^n(2) = \exp(...(\exp(2))$</span>.</p>

<p>Especially from the view of parametrised complexity, this would be interesting.</p>

<p>I'm aware, that these problems can also be solved via Cylindrical Algebraic Decompositions, but I'am really interested in the running time of the original method.</p>

<p>The comments already mention how the formula roughly looks like, but don't give a source.</p>

CC BY-SA 4.0
2020-04-14T14:35:12.877Z
Yes, the running time is a power tower $\exp^{O(n)}(2)$. More precisely, it should be something like $\exp^{O(m)}(n)$, where $n$ is the overall length of the formula, and $m$ is the number of quantifiers.
Emil Jeřábek
CC BY-SA 4.0
2020-04-14T16:06:11.163Z
@EmilJeřábek: Thanks, do you have a (citable) source for that?
If you write this as a full answer, I can put the checkmark. :)
Hennich
CC BY-SA 4.0
2020-05-19T15:40:09.007Z
I’m sorry, but looking up references is very time consuming, I have no time for that now.
Emil Jeřábek
<parameterized-complexity>
Running time of Tarski Quantifier Elimination
Hennich
# Running time of Tarski Quantifier Elimination

(Asked by: username_0 on 2020-04-14)

I'm looking for some formula/expression in a citable resource, that gives the running time for Tarski's quantifier elimination.

In my search, I only found the statement "it's not elementary" on several pages and papers.
But given the explanation on <https://en.wikipedia.org/wiki/ELEMENTARY>, this could allow for a "power tower" like $\exp^n(2) = \exp(...(\exp(2))$.

Especially from the view of parametrised complexity, this would be interesting.

I'm aware, that these problems can also be solved via Cylindrical Algebraic Decompositions, but I'am really interested in the running time of the original method.

The comments already mention how the formula roughly looks like, but don't give a source.

**Tags:** parameterized-complexity

> **Comments:**
> **username_1**: Yes, the running time is a power tower $\exp^{O(n)}(2)$. More precisely, it should be something like $\exp^{O(m)}(n)$, where $n$ is the overall length of the formula, and $m$ is the number of quantifiers.  
> **username_0**: @EmilJeřábek: Thanks, do you have a (citable) source for that? If you write this as a full answer, I can put the checkmark. :)  
> **username_1**: I’m sorry, but looking up references is very time consuming, I have no time for that now.  

---

## 0 answers

