I'm going to define an exponential polynomial of degree $k$ as a function $f$ of the form

$f(x) = \sum_{i=1}^k c_ie^{\alpha_ix}$ ($\alpha_i$s real).

My first question is: is there an algorithm for counting the number of real roots of such an expression, with complexity depending only on the degree $k$?

I strongly suspect that the answer to this question is yes, and that the answer is known (seeing as Tarski's exponential function problem is all but solved), but I can't find it described anywhere.

My second question is: can somebody tell me what this algorithm is? Or give me a hint?

I vaguely remember reading somewhere that there was a known method analogous to the method of Sturm chains for polynomials... But I haven't been able to figure out what it should be, nor have I been able to find where I read that claim. My best guess is that we can get rid of terms of such an expression by first dividing $f$ by an exponential $e^{\alpha x}$ to make a term constant, differentiating, and then multiplying by that same exponential. If we call this operation $D_{\alpha}$, we get $D_{\alpha}f(x) = \sum_{i=1}^k c_i(\alpha_i-\alpha)e^{\alpha_ix}$. The nice thing is that $D_{\alpha}f$ acts analogously to the derivative of $f$, i.e. between any consecutive zeroes of $f$ there is a zero of $D_{\alpha}f$. The problem is that I can't think of a good analogue to the division algorithm for exponential polynomials (maybe we don't need one?).

I'm going to define an exponential polynomial of degree $k$ as a function $f$ of the form

$f(x) = \sum_{i=1}^k c_ie^{\alpha_ix}$ ($\alpha_i$s real).

My first question is: is there an algorithm for counting the number of real roots of such an expression, with complexity depending only on the degree $k$?

I strongly suspect that the answer to this question is yes, and that the answer is known (seeing as Tarski's exponential function problem is all but solved), but I can't find it described anywhere.

My second question is: can somebody tell me what this algorithm is? Or give me a hint?

I vaguely remember reading somewhere that there was a known method analogous to the method of Sturm chains for polynomials... But I haven't been able to figure out what it should be, nor have I been able to find where I read that claim. My best guess is that we can get rid of terms of such an expression by first dividing $f$ by an exponential $e^{\alpha x}$ to make a term constant, differentiating, and then multiplying by that same exponential. If we call this operation $D_{\alpha}$, we get $D_{\alpha}f(x) = \sum_{i=1}^k c_i(\alpha_i-\alpha)e^{\alpha_ix}$. The nice thing is that $D_{\alpha}f$ acts analogously to the derivative of $f$, i.e. between any consecutive zeroes of $f$ there is a zero of $D_{\alpha}f$. The problem is that I can't think of a good analogue to the division algorithm for exponential polynomials (maybe we don't need one?).

Edit: When I say that Tarski's exponential function problem is "all but solved," I mean that all that is missing from the full solution is a proof of Schanuel's conjecture. I'm not saying that Schanuel's conjecture is easy, but given this result it seems to me that we should be able to describe some sort of explicit algorithm for deciding problems like this one, although the proof of correctness of such an algorithm might require us to assume Schanuel's conjecture holds.