Software to decide equality between expressions involving powers and trigonometry Given two expressions A and B involving integers, $\pi$, powers to rational exponents, and cosine, is there a software that determines if A = B? (Previous question asked A > B, but the bottleneck is equality.)
I am aware of the long-standing sum-of-square-roots problem in complexity theory. I am asking if there is a software implementation of a sound algorithm, which may take a long time or even not always terminate. As far as I know, standard math software, even if symbolic, resorts to decimal expansion to determine if A > B; but without mathematical guarantee.
 A: I believe that what you are looking for is MetiTarski.  It is written (in part) by Larry Paulson, principal author of the theorem prover Isabelle.
Note also that Maple has an interval arithmetic package (evalr), which can also be used to show that certain inequalities are true.  Maple does not use 'raw' floating point arithmetic to decide exact problems - that would be horribly unsound.
A: In Maple, you might try the probabilistic equivalence-tester testeq. For example:

testeq(407-768*cos(1/5*Pi)-716*cos(1/7*Pi)-364*cos(11/35*Pi)-170*cos(1/35*Pi)+170*cos(6/35*Pi)+364*cos(4/35*Pi)-594*cos(9/35*Pi)+594*cos(16/35*Pi)+692*cos(2/5*Pi)+670*cos(2/35*Pi)+670*cos(12/35*Pi)-440*cos(3/35*Pi)-440*cos(17/35*Pi)+246*cos(8/35*Pi)-246*cos(13/35*Pi)-292*cos(3/7*Pi)+486*cos(2/7*Pi)=0);

true
EDIT: For trigonometric polynomials in rational multiples of $\pi$ with rational coefficients, equality can be checked algebraically. Let $x = \sum_{n=1}^n a_j \cos(b_j \pi/m)$ where $m$, $a_j$ and $b_j$ are integers, $0 \le b_j < 2m$. Then if $\omega=e^{i\pi/m}$ we have $x=\sum_{j=1}^n a_j(\omega^{b_j}+\omega^{−b_j})/2$. So $x=0$ iff the minimal polynomial of $\omega$, which is the cyclotomic polynomial $\Phi_m(z)$, divides $\sum_{j=1}^n a_j (z^{2m+b_j} + z^{2m-b_j})$.
