What would be a good writeup for understanding term-rewriting? (My current background level: I understand most of what OP has listed in "actually useful" and "can run into", and "automata theory" from the third list.)
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. :-)
