Testing whether an expression (say, on the real or complex numbers), with or without variables, is known to be difficult. There is an semi-algorithm by Daniel Richardson to solve it for the exp–log setting, but even that only terminates for all inputs iff Schanuel's conjecture is true. Adding some more things like $\sin$ and $\pi$ makes it definitely undecidable.
So I was wondering: What do computer algebra systems like Mathematica and Maple do in practice if they need to decide whether a given expression (possibly containing variables) is or is not zero? (for instance, the user is asking for the limit of $c^2 x$ for $x\to\infty$ where $c$ is some more complicated expression, possibly containing parameters).
I'm sure they employ lots of heuristics like simplification rules and approximation, but do they also implement more systematic checks, such as Richardson's algorithm?
I would very much appreciate citable sources if at all possible, but even just some ‘hearsay’ would be very helpful.
I can only answer for Maple. No, it does not implement Richardson's algorithm.
First, in Maple, zero equivalence (by default) is done by very fast, and thus very weak, routines. Essentially it treats all symbolic expressions as being polynomials over $\mathbb{Q}$ (i.e. any symbolic expression is treated as a fresh variable, where 'new' means that it hashes to something distinct), without normalization. So $(x-1)\cdot(x+1)$ is not equal to $x^2-1$, but $2\cdot(x+1)$ is equal to $2x+2$.
Second, you can ask for more computation to happen, by applying routines like $\texttt{normal}$, $\texttt{simplify}$ and so on.
Third, internally to Maple, the function most often used to test zero equivalence is $\texttt{testeq}$, which is a probabilistic routine, based on reductions in $\mathbb{Z}_p$, see [1] for more details. The online help page can be helpful too.
Lastly, and this is not so well known, the most powerful zero-equivalence check in Maple is actually contained in its $\texttt{solve}$ routine! This has never been properly documented, and accessing it externally is tricky. One way is via $\texttt{is}$, part of the $\texttt{assume}$ system - but that too is tricky, as one might get caught be a heuristic meant to "fail fast" and not get into the more complex routines. Via setting $\texttt{_EnvTryHard}$ to true can sometimes help.
[1] Gonnet, Gaston. "Determining Equivalence of Expressions in Random Polynomial Time." Proceedings of the 16th ACM Symposium on the Theory of Computing. Washington DC. April 1984. pp. 334-341.