Term-Ersetzung und Computeralgebra

Regeln (Term-Ersetzungs-System) für das Differenzieren:

$$\notin$$ D_x(A + B) = D_x(A) + D_x(B) D_x(A ^. B) = ..., D_x(A/B) =... D_x(log x) = 1/x, D_x(sin x) = cos x,...

Dazu braucht man aber noch Vereinfachungsregeln.

Wie drückt man die Kettenregel D_x(f (g(x)) = ... aus?

Hier sind f und g Variablen, aber zweiter Ordnung (bezeichnen Funktionen).

Regeln für das Integrieren?

Existenz und Eindeutigkeit von Normalformen?