Gleichungssysteme (Syntax)

• Def: Gleichungssystem E über Signatur Σ ist Menge von Paaren (l, r)∈Term(Σ, V)², geschrieben l $\approx$ r
• Def: die Relation $\approx_{E}^{}$ ist (→_E∪→_E^-)^*. (alternativ: ↔_E^*)
• Bsp: E₁ = {f⁵(a) $\approx$ a, f³(a) $\approx$ a}. Zeige f (a) $\approx_{{E_1}}^{}$ a.

  Bsp: E₂ = {f (f (x)) $\approx$ g(x)}. Zeige f (g(x)) $\approx_{{E_2}}^{}$ g(f (x)).

  Bsp: Die Relation $\approx_{{D_i}}^{}$ ist entscheidbar für

  • D₁ = {f (f (x, y), z) $\approx$ f (x, f (y, z))}
  • D₂ = {f (f (x, y), z) $\approx$ f (x, f (y, z)), f (x, y) $\approx$ f (y, x)}

  $\approx_{C}^{}$ ist nicht entscheidbar für C = {A(A(K, x), y) $\approx$ x, A(A(A(S, x), y), z) $\approx$ A(A(x, z), A(y, z))}