Termersetzungssysteme

• Programm R = Menge von Regeln
• Regel = Paar (l, r) von Termen mit Variablen
• Relation →_R ist Menge (t, t') mit
  • es existiert Position p in t
  • es existiert Substitution σ : Var(l )→Term(Σ)
  • es existiert (l, r)∈R
  • so daß t|_p = lσ und t' = t[p : = rσ].

Hilfsbegriffe:

• Position: Folge von natürlichen Zahlen
• t|_p: der Teilterm von t an Position p
• t[p : = s] : wie t, aber mit Term s an Position p
• Substitution σ: Abbildung Var→Term(Σ)
• lσ: wie l, aber statt v immer σ(v)