Motivation (II)

gesucht ist Entscheidungsverfahren für s $\approx_{E}^{}$ t

Plan: Vergleich der →_E -Normalformen von s, t .

Probleme: 1. Existenz und 2. Eindeutigkeit der Nf.

Lösung:

• (Ziel): 1. Termination und 2. Konfluenz
• (Verfahren): Vervollständigung.

Bsp: E = aba $\approx$ ε , abbbaa $\approx_{E}^{}$ bba ?      Orientiere aba→ε ,

nicht konfluent wegen ba←ababa→ab ,

neue Regel ba→ab ,

nicht konfluent wegen ..., neue Regel ...,

konfluent? terminierend? NFs von s, t ?