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.
Unifikation
Ich habe mal die Unifikations Aufgabe von der Probleklausur WS12/13 gemacht, hier der Lösungsversuch:
f(g(Y),X,Y) = f(g(Z), g(Z),X)
g(Y) = g(Z), X = g(Z), Y= X ← decomp
Y = Z, X = g(Z), Y = X ← decomp
X = Z, X = g(Z), Y = X ← elim
X = Z, Z = g(Z), Y = X ← elim
mgu[ X → Z, Y->X]
stimmt das so ? bzw wenn man Z = g(Z) hat, fällt das dann einfach weg ?
Das ganze ist nicht unifizierbar, weil du kein (endliches) Z finden kannst, das Z=g(Z) erfüllt.
Regel im Algo dafür dürfte sein: Z \in FV(g(Z))
Genau.
Im inoffiziellen Skript sieht die übrigens so aus:
Du kannst daher also das Z nicht eliminieren.
danke für die Antworten, ich schreib mir die regeln wohl besser doch nochmal auf für die klausur 