Kritische Paare

Für ein Termersetzungssystem R über $\Sigma$: falls

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

  d. h., es existiert mgu $\sigma$ mit l₁[p]$\sigma$ = l₂$\sigma$

• falls (l₁$\to$r₁) = (l₂$\to$r₂) (vor Umbenennung), dann p $\neq$ $\epsilon$
• dann heißt (r₁$\sigma$,(l₁$\sigma$)[p : = r₂$\sigma$]) kritisches Paar von R.

Ein kritisches Paar (s, t) heißt zusammenführbar, falls $\exists$u : s$\to_{R}^{*}$u $\wedge$ t$\to_{R}^{*}$u.

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