Unifikation--Begriffe

• Signatur Σ = Σ₀∪…Σ_k mathend000#,
• Term(Σ, V) mathend000# ist kleinste Menge T mathend000# mit V⊆T mathend000# und ∀0≤i≤k, f∈Σ_i, t₁∈T,…, t_i∈T : f (t₁,…, t_i)∈T mathend000#.
• Substitution: partielle Abbildung σ : V→Term(Σ, V) mathend000#, so daß kein v∈domσ mathend000# in imgσ mathend000# vorkommt,
• Substitution σ mathend000# auf Term t mathend000# anwenden: tσ mathend000#
• Produkt von Substitutionen: so definiert, daß t(σ₁oσ₂) = (tσ₁)σ₂ mathend000#