Unifikation (Logik) - de.LinkFang.org

Unifikation (Logik)

Unifikation ist eine Methode zur Vereinheitlichung prädikatenlogischer Ausdrücke. Zwei Ausdrücke werden unifiziert, indem ihre Variablen so durch geeignete Terme ersetzt werden, dass die resultierenden Ausdrücke gleich sind. Die Unifikation hat insbesondere in der Computerlogik und Computerlinguistik eine größere Bedeutung erlangt. So nutzt etwa die Inferenzmaschine des Prolog-Interpreters Unifikation. In der Computerlinguistik gibt es sogenannte Unifikationsgrammatiken, die sich auf dieses Konzept stützen. Auch beim Theorembeweisen spielt Unifikation eine große Rolle.

Als Basisoperation liegt der Unifikation die Substitution zu Grunde. Im Rahmen der Prädikatenlogik bedeutet eine Substitution σ innerhalb eines gegebenen Ausdrucks die Ersetzung einer Variablen durch einen Term, in dem diese Variable nicht vorkommen darf. Die Variable wird gewissermaßen durch den Term „instanziiert“.

Wird eine Menge von Ausdrücken \{A_{1},A_{2},\ldots ,A_{n}\} durch eine Substitution σ zu einem äquivalenten Ausdruck substituiert, d. h. \sigma (A_{1})\equiv \sigma (A_{2})\equiv \cdots \equiv \sigma (A_{n}), so bezeichnet man σ als Unifikator dieser Ausdrucksmenge. Die Anwendung eines Unifikators auf diese Menge bezeichnet man als Unifikation. Nicht alle Ausdrucksmengen können unifiziert werden.

Inhaltsverzeichnis

Beispiel


Gegeben seien die Ausdrücke A_{1}=\left(X,Y,f(b)\right) und A_{2}=\left(a,b,Z\right). Großbuchstaben stehen dabei für Variablen und Kleinbuchstaben für atomare Ausdrücke.

Ersetzt man in A_{1} nun X durch a, Y durch b und in A_{2} Z durch f\left(b\right), so sind sie gleich oder unifiziert. Man erhält

\sigma (A_{1})=\left(a,b,f(b)\right)
\sigma (A_{2})=\left(a,b,f(b)\right)

mit

\sigma =\{X\mapsto a,Y\mapsto b,Z\mapsto f(b)\}.

Kleinster gemeinsamer Unifikator


Zu einer Menge von Ausdrücken existieren gewöhnlich mehrere Unifikatoren. Man nennt einen Unifikator \mu kleinster gemeinsamer Unifikator oder allgemeinster Unifikator, wenn es für jeden anderen Unifikator \sigma eine Substitution \tau gibt mit \sigma =\tau \circ \mu . Dieser ist natürlich nicht notwendigerweise eindeutig.

Mittels des Algorithmus von Robinson nach John Alan Robinson kann man zu unifizierbaren Ausdrücken einen kleinsten gemeinsamen Unifikator finden.

Unifikationsalgorithmus


Es folgt eine Darstellung des Unifikationsalgorithmus in Pseudocode:

Eingabe: Menge von Ausdrücken A
Ausgabe: allgemeinster Unifikator sub
sub := ∅
while |sub(A)| > 1 do begin
  Durchsuche die Ausdrücke sub(A) von links nach rechts,
  bis die erste Position gefunden ist, wo sich zwei Ausdrücke
  in einem Zeichen unterscheiden.
  if keines der beiden Zeichen ist eine Variable then
    Gib "nicht unifizierbar" aus. STOP
  else begin
    Sei X die Variable und t der im anderen Ausdruck beginnende Term
    (kann auch Variable sein)
    if X kommt in t vor then
      Gib "nicht unifizierbar" aus. STOP
    else sub := sub[X/t] (sub und [X/t] werden hintereinander ausgeführt)
  end
end
Gib sub aus.

Literatur





Kategorien: Logik



Quelle: Wikipedia - https://de.wikipedia.org/wiki/Unifikation (Logik) (Autoren [Versionsgeschichte])    Lizenz: CC-by-sa-3.0

Veränderungen: Alle Bilder und die meisten Designelemente, die mit ihnen in Verbindung stehen, wurden entfernt. Icons wurden teilweise durch FontAwesome-Icons ersetzt. Einige Vorlagen wurden entfernt (wie „Lesenswerter Artikel“, „Exzellenter Artikel“) oder umgeschrieben. CSS-Klassen wurden zum Großteil entfernt oder vereinheitlicht.
Wikipedia spezifische Links, die nicht zu Artikeln oder Kategorien führen (wie „Redlink“, „Bearbeiten-Links“, „Portal-Links“) wurden entfernt. Alle externen Links haben ein zusätzliches FontAwesome Icon erhalten. Neben weiteren kleinen Designanpassungen wurden Media-Container, Karten, Navigationsboxen, gesprochene Versionen & Geo-Mikroformate entfernt.


Stand der Informationen: 21.10.2019 10:23:12 CEST - Wichtiger Hinweis Da die gegebenen Inhalte zum angegebenen Zeitpunkt maschinell von Wikipedia übernommen wurden, war und ist eine manuelle Überprüfung nicht möglich. Somit garantiert LinkFang.org nicht die Richtigkeit und Aktualität der übernommenen Inhalte. Sollten die Informationen mittlerweile fehlerhaft sein oder Fehler in der Darstellung vorliegen, bitten wir Sie darum uns per zu kontaktieren: E-Mail.
Beachten Sie auch : Impressum & Datenschutzerklärung.