Is there an algorithm for deciding big/little-O queries? Consider the following question:

Is $2^{o(\log n)} = o(n^c)$ for every constant $0 < c < 1$?

I can try to answer this question using basic limits to get that the answer is "yes." I can also put a query of the following form into Wolfram alpha: What is $\lim_{n \to \infty} \frac{2^{\log^{0.999}n}}{n^{0.0001}}$? And it will spit out zero, while it fails to answer the first question because it apparently does not contain information about little-o notation or I don't know how to specify that this is what I want.
My question is: given an input query of the above form, that is, two expressions composed as an elementary combination of elementary functions and Big/Little-O (or $\omega, \Omega, \Theta$), is the problem of answering such queries decidable? Is it in P? If so, could you provide a reference to the algorithm? Are there any existing mathematical software packages that can answer queries of this form?
 A: Theorem: Consider the following inductively defined set of functions $\mathcal{F \subseteq \mathcal{C}(\mathbb{R})}$:


*

*If $q\in \mathbb{Q}$ is a rational number, then the constant function $const_q: x \mapsto q$ is in $\mathcal{F}$.

*$const_\pi$ and $const_{ln(2)}$ are in $\mathcal{F}$.

*Identity function $x\mapsto x$ is in $\mathcal{F}$.

*If $f,g\in \mathcal{F}$, then $f+g$ and $f\cdot g$ are also in $\mathcal{F}$.

*If $f\in\mathcal{F}$, then $\sin \circ \, f$, $\exp \circ \, f$, and $x \mapsto \vert f(x) |$ are in $\mathcal{F}$.

*$f\in\mathcal{F}$, then $\ln \circ \,f$ is in $\mathcal{F}$.


Then the question whether $f(n)\in \mathcal{O}(1)_{n\to\infty}$ with $n\in\mathbb{N}$ is undecidable. In particular, there is no algorithm that could automatically answer $f(n) \in \mathcal{O}(g(n))$ queries for general functions that are built from rational polynomials, absolute value function, the sine, the logarithm, and the constants $\ln(2)$ and $\pi$.
Proof: The idea is to transform statements like "$A(x) = 0$" into equivalent statements "$\Phi[A](n) \in \mathcal{O}(1)_{n\to\infty}$" with some functional $\Phi[-]$, and then invoke Richardson's theorem. For this, we need a sequence that repeatedly "scans" the entire real line. Then we can use this sequence to look for deviations of $A(x)$ from $0$, and amplify the errors with a divergent function. If the errors remain bounded, i.e., if $\Phi[A](n)\in \mathcal{O}(1)$, we know that $A$ is constant $0$. Otherwise, we know it is not $0$.
Consider the sequence $y_n := \ln(n)\cdot\sin(\ln(n))$ for $n\in\mathbb{N}$.
It is relatively easy to show that whenever a sequence $a_n$ has the property $\lim_{n\to\infty}a_{n+1}(a_{n+1} - a_n) = 0$, the set $\{a_n\cdot\sin(a_n)\}_n$ is dense in $\mathbb{R}$. Since $\ln(n+1) - \ln(n)\in \mathcal{O}(1/n)$, and $\lim_{n\to\infty} \frac{\ln(n+1)}{n} = 0$, $\{y_n\}_n$ is dense in $\mathbb{R}$.
Now, let $A\in\mathcal{F}$ arbitrary. Consider $\Phi[A](n) := n\cdot A(y_n)$. Suppose $A\neq 0$. Then there is some $x_0\in\mathbb{R}$ with $A(x_0) \neq 0$. Since all functions of $\mathcal{F}$ are continuous, there must be a neighbourhood $(a,b)$ of $x_0$ such that $|A(x)| > |A(x_0) / 2|$ for all $x\in(a,b)$. Since $\{y_n\}_n$ is dense in $\mathbb{R}$, there must be a subsequence $n_k\in\mathbb{N}$ with $y_{n_k}\in(a, b)$. In particular, $|n_k\cdot A(y_{n_k})| > n_k\cdot |A(x_0)| / 2 \to \infty$ for $k\to\infty$. Thus, $\Phi[A](n) \not\in\mathcal{O}(1)$. On the other hand, if $A = 0$, then $\Phi[A](n)$ is clearly also just $0$, and therefore in $\mathcal{O}(1)$. This yields the equivalence $A = 0 \Leftrightarrow \Phi[A](n)\in\mathcal{O}(1)$. If we could algorithmically decide whether $\Phi[A](n)\in\mathcal{O}(1)$, we could also decide whether $A = 0$. By Richardson's theorem, the latter problem is undecidable. Therefore, there is no algorithm that can answer queries of the form $f\in \mathcal{O}(1)$ for $f\in\mathcal{F}$. $\blacksquare$
Remark: The first five term-construction rules are copied from Richardson's theorem. However, in the rule number 6), the logarithm is added so that we can construct the sequence $\ln(n)\cdot\sin(\ln(n))$ with the property that $\{\ln(n)\cdot\sin(\ln(n))\}_n$ is dense in $\mathbb{R}$. 
If one somehow could show that $\{n\cdot \sin(n)\}$ is dense in the real line, one wouldn't need the sixth rule. However, to show that $\{n\cdot \sin(n)\}_n$ is dense, one seemingly needs some number-theoretic properties of $\pi$ (see here: Is n sin(n) dense in R?), whereas the proof that $\{\ln(n)\cdot\sin(\ln(n))\}_n$ is dense requires only some basic calculus.

Conclusion: the much easier problem to tell whether $f\in \mathcal{O}(1)$ is already undecidable. If one allows $\mathcal{O},o,\Omega,\Theta$ on the left hand side, the problem obviously doesn't get any easier, so the answer to you original question is: the problem is undecidable "in general". However, one might be able to find some algorithms for subsets of $\mathcal{F}$. For example, I don't know whether the above argument remains valid if one leaves out the absolute value function or the logarithm. To understand this, one should probably look at the various versions of Richardson's theorem.

(obsolete proof-sketch)
[The following two paragraphs contain my first attempt to answer this question. The idea is similar, but the premises are unnecessarily strong, and the proof as a whole contains some subtle flaws]
Suppose $f$ is some analytic "elementary" function on an interval $I$. Find a point $c\in I$ and a positive $r > 0$ such that the subinterval $[c - r, c + r]$ is contained in $I$. 
Now consider the function $A(x) = x \cdot (f(c + r \sin(x)) -f(c))$.
Clearly, if $f(y) \neq f(c)$ for some $y\in I$, this function would eventually blow up for $x\to\infty$. If it does not blow up, $f$ must be constant on $[c - r, c + r]$, and thus it must be constant everywhere (because an analytic function is completely determined by the values in the interval $[c - r, c + r]$). Now suppose that we have an algorithm that can answer queries as those described in your question. Let the algorithm answer the question whether $A(x) \in O(1)$. If it says "yes", we know that $A(x)$ does not blow up, and thus $f$ is constant. If it says "no", we know that $f$ is not constant.
Thus, we would obtain an algorithm that can decide for all analytic functions $f(x)$ whether they are constant or not. This is a contradiction to Richardson's theorem (https://en.wikipedia.org/wiki/Richardson's_theorem), which says that such questions are undecidable in general.
(/obsolete proof-sketch)
