It is well-known that CAS are able to perform operations like formal differentiation (relatively easily) and formal integration (via the Risch algorithm) in an algorithmic way.
But is there anything equivalent for the resolution of transcendental equations, be it for the expression of the roots, or for root isolation ?
Of course root computation is known to be feasible symbolically for polynomials up to degree four and generally infeasible for higher degrees, and some equations can be transformed into polynomial form by variable substitution. For instance,
$$8^x-7\cdot2^x-6=0$$ has closed-form expression for the root(s).
But is there any theory for general equations, discussing the number of roots, approximations to the roots or the exact roots themselves ? For instance, it is an easy matter to prove that $\sin x=x$ has a single root at $x=0$ or that $\tan x=x$ has single roots in intervals of length $\pi$. But can a CAS infer this ?
Acceptable solutions could be purely symbolic, but also numerical, provided in the latter case guarantees are given that all roots are enumerated.
What is known about this topic ?