Formale Schreibweise Unifikation

Bachelor Grundlagen der Logik in der Informatik
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

Formale Schreibweise Unifikation
Gab es Aussagen in den Übungen, wie die Unifikation formal aufs Papier gebracht werden soll? Ich habe jetzt mehrere Schreibweisen gefunden. Der Lösungsversuch der Probeklausur unterscheidet sich z.B. von meiner Mitschrift vom letzten Semester (dieses Semester Übung 5, Aufgabe 5.3). Ich hatte es wie folgt notiert:

Angabe: 
link2(link3(a,Y,Z),X) = link2(X,link3(a,Y,Y))

Lösung: 
{link2(link3(a,Y,Z),X) = link2(X,link3(a,Y,Y))}
decomp => {link3(a,Y,Z) = X; X=link3(a,Y,Y)}
elim => {link3(a,Y,Z)=link3(a,Y,Y); x=link3(a,Y,Y)}
decomp => {a=a; Y=Y; Z=Y; x=link3(a,Y,Y)}
=> {Z=Y; X=link3(a,Y,Y)}

Unifizierbar, mgu [Z->Y; X->link3(a,Y,Y)]

Wie wird es denn vom Lehrstuhl gewünscht?

3

Es gibt diverse Schreibweisen, ja. Aber einen ⇔ hab ich da noch nie gesehen …
Am besten, ihr verwendet die Schreibweise, die wir in diesem Semester auch verwendet haben (Mengen von Gleichungen als {C ≐ D, E ≐ F, …}, dann mit den Regeln beschriftete Übergänge (wenn ich recht erinnere mit Doppelpfeil)). Mit anderen Worten: Die Schreibweise, die du da verwendet hast, bloß mit nem Punkt über dem = :wink:

Edit: eine Kleinigkeit noch: im mgu (wie auch sonst in Substitutionen, Umgebungen etc.) immer [X ↦ Y] schreiben, nicht [X → Y]. (Für Substitutionen existiert außerdem die Schreibweise [Y/X] für [X ↦ Y], wichtig dabei die Reihenfolge)

1 Like