Unifikation

Unifikation zweier Terme: Ersetzung (Substitution) der Variablen in den Termen derart, dass die so entstandenen Zeichenfolgen gleich sind

• Zwei Terme sind unifizierbar, wenn:
  • Sie beide dieselbe Individuenkonstante sind
  • Einer von ihnen eine freie Variable ist
  • Beide komplexe Terme sind mit folgenden Eigenschaften:
    • der Funktor ist derselbe
    • die Anzahl Parameter (Stelligkeit) ist gleich
    • deren Argumente sind paarweise unifizierbar