Gleichungssysteme (Syntax)

Def: ein Gleichungssystem E über einer Signatur Σ ist eine Menge von Paaren (l, r)∈Term(Σ, V)² , geschrieben l $\approx$ r

Def: die Relation $\approx_{E}^{}$ ist (→_E∪→_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))}