Motivation für Polynom-Reduktion

• Ansatz für Entscheidungsverfahren für g₁≡_Bg₂
  • Normalformen bestimmen g₁→_B^*g₁', g₂→_B^*g₂'
  • und vergleichen g₁' = g₂'$\iff$g₁≡_Bg₂
  dazu muß →_B terminieren und konfluent sein
• g→_Bh falls ∃f∈B, so daß h = g - c⋅f

  (nach Ideal-Definition folgt daraus g≡_Bh)

• Termination: geeignete Ordnung, so daß g > h
• (lokale) Konfluenz: Zusammenführen kritischer Paare durch Ergänzung der Basis