Motivation, Beispiel

• gegeben E, gesucht: Entscheidungsverfahren für s $\approx_{E}^{}$ t

  Bsp: E = {aba→ε}, s = abbbaa, t = bba.

  Plan: Vergleich der E-Normalf. von s, t. Aber: ¬(UN(E)),

• Lösung: Vergleich der →_F-Normalformen für ein F mit
  • Hinzufügen von Regeln E = E₀⊆E₁⊆...⊆E_n = F
  • Invariante: E_i⊆( $\approx_{E}^{}$ ) und SN(E_i) (dann ( $\approx_{{E_i}}^{}$ ) = ( $\approx_{E}^{}$ ))

  • Ziel: WCR(F) (dann gilt CR(F) und UNC(F))
• Bsp: ba←_Eababa→_Eab, also ba $\approx_{E}^{}$ ab,

  E₁ = E∪{ba→ab}, SN(E₁) wg. length-lex-order

  E₁ nicht lokal konfluent wegen ..., neue Regel ...,