Unifikation (Logik)
aus Wikipedia, der freien Enzyklopädie
Unifikation ist eine Methode zur Vereinheitlichung prädikatenlogischer Ausdrücke. Diese 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 (Logik) 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 {A1,A2,...,An} durch eine Substitution σ zu einem äquivalenten Ausdruck substituiert, d.h. , so bezeichnet man σ als Unifikator dieser Ausdrucksmenge. Die Anwendung eines Unifikators auf diese Menge bezeichnet man als Unifikation.
Nicht alle Ausdrücke können unifiziert werden!
Inhaltsverzeichnis |
[Bearbeiten] Beispiel
Gegeben seien die Ausdrücke A1 = (X,Y,f(b)) und A2 = (a,b,Z)
Ersetzt man in A1 nun X durch a, Y durch b und in A2 Z durch f(b), so sind sie gleich oder unifiziert.
[Bearbeiten] Kleinster gemeinsamer Unifikator
Zu einer Menge von Ausdrücken existieren gewöhnlich mehrere Unifikatoren. Man nennt einen Unifikator μ kleinster gemeinsamer Unifikator oder allgemeinster Unifikator, wenn es für jeden anderen Unifikator σ eine Substitution τ gibt mit
Mittels des Algorithmus von Robinson nach John Alan Robinson kann man zu unifizierbaren Ausdrücken einen kleinsten gemeinsamen Unifikator finden.
[Bearbeiten] Unifikationsalgorithmus
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] end end Gib sub aus.
[Bearbeiten] Literatur
- J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM. 1965 ACM Press