Termersetzungssysteme

• Daten = Terme (ohne Variablen)
• Programm R = Menge von Regeln

  Bsp: R = {(f (Z(), y), y),  (f (S(x), y), S(f (x, y)))}

• Regel = Paar (l, r) von Termen mit Variablen

• Relation →_R ist Menge aller Paare (t, t') mit
  • es existiert (l, r)∈R
  • es existiert Position p in t
  • es existiert Substitution σ : (Var(l )∪Var(r))→Term(Σ)
  • so daß t[p] = lσ und t' = t[p : = rσ].