Kritische Paare

Für ein Termersetzungssystem R über Σ : falls

• (l₁→r₁) und (l₂→r₂) sind Regeln in R ohne gemeinsame Variable (ggf. vorher umbenennen!)
• es gibt p∈Pos(l₁) so daß l₁[p] und l₂ unifizierbar sind

  d. h., es existiert mgu σ mit l₁[p]σ = l₂σ

• falls (l₁→r₁) = (l₂→r₂) (vor Umbenennung), dann p≠ε
• dann heißt (r₁σ,(l₁σ)[p : = r₂σ]) kritisches Paar von R .

Ein kritisches Paar (s, t) von R heißt zusammenführbar, falls ∃u : s→_R^*u∧t→_R^*u .

Satz: ein Termersetzungssystem ist genau dann lokal konfluent, wenn alle kritische Paare zusammenführbar sind.