Could you also recommend something on how symbolic computation works? I have used computer algebra systems like Mathematica for long; would like to understand how it works internally.
I currently understand some basics like DPLL, semantic first-order unification, methods of solving specific equation systems like linear systems, numerical differential equations, etc. I am missing at least how the "top-level" of symbolic computation works.
For example, from what I currently understand, first-order semantic unification can find "x = Cos[y]" from "Sin[x] = Sin[Cos[y]]", but cannot solve "Sin[x] = Cos[x]" for x, and cannot simplify "[(Sin[x])^2 + (Cos[x])^2] = 1" to True.
I am hoping to find something simpler than reading through SymPy source code. :-)
