Motivation

• gibt es unendliche Ableitungen für ...?
  • a→b,  ba→ab,  ba→aab,   aa→aba,  100→00110
  • A(A(D, x), y)→A(x, A(x, y))
  • Regeln zum symbolischen Differenzieren
  • zum Auswerten o. Vereinfachen Boolescher Ausdrücke
  • beliebiges Programm (TM (SRS), funktional (TRS))
• Anwendung (später): Vervollständigungs-Algorithmus

  (zum Entscheiden der syntaktischen Kongruenz $\approx_{E}^{}$)

  Invariante: das (aktuelle) System terminiert
  (Ziel: ...und ist konfluent)