[alok-g]

Thanks!

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. :-)

[nextos]

Peter Norvig's PAIP book has a chapter devoted to Student, a computer algebra system. It's very didactic:

http://norvig.com/paip/student.lisp