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.
Probeklausur - Aufgabe 3 (Unifikation)
Hi,
sehe ich das richtige, dass Aufgabe 3 sehr kurz ist?
Ich ersetze erst X durch h(Z) => h(Z)/X
Dann ersetze ich Z durch h(W) => h(W) /Z
Wenn ich das dann noch ineinander einsetzte habe ich mgu = [h(h(W))/X, h(W)/Z]
Stimmt das so oder habe ich da was falsch verstanden?
Ja stimmt so, ich wuerde aber raten in der Klausur die Schritte des Algorithmus nach und nach anzuwenden und zu nennen, dann ist man bei der sicheren Seite punktemaessig.
Edit: Den Loesungsversuch der Glolop-Uebungsgruppe unter anderem auch zu der Unifikations-Aufgabe gibts hier.
Zu dem verlinkten Lösungsversuch…Ist es bei Fitch erlaubt, dass man alles mögliche als Anfangsannahme nehmen darf und am Ende nur die Formel rauskommen muss, die wir eben mit Fitch beweisen sollen?
Weil meine Lösung wäre das Gegenteil anzunehmen am Anfang und dann eigentlich exakt so fortfahren wie im verlinkten Lösungsversuch. Sind zwar ein paar Zeilen mehr, ab so habe ich es auch in den Übungen immer gemacht.
Aber wenn ich von Anfang einfach nur den ersten Teil annehmen darf, dann würde ich mir natürlich ein wenig Arbeit sparen.
Ich bin mir nicht wirklich sicher, ob ich deine Frage richtig verstehe:
Du möchtest wissen, ob du (A → (B v C) and (neg(A and B))) annehmen darfst?
Klar darfst du das!
Du darfst alles annehmen, was du möchtest!
Ist in diesem Fall aufgrund der zu zeigenden Implikation durchaus sinnvoll.
Die Unifikationsaufgabe erscheint mir in der Tat etwas kurz, verglichen mit den anderen Aufgaben. Weiß vielleicht jemand aus dem vorherigen Semester noch, wie genau das in der Klausur gefordert wird?
Was für Zwischenschritte muss man machen?
All. Frage zur Unifikation
Gibt es eine vorgebene Reihenfolge für die Ersetzung?
Bsp.:
g(X, X, f(Z)) ≐ g(Y, X, f(X)) [X/Y]
g(X, X, f(Z)) ≐ g(X, X, f(X))
g(X, X, f(Z)) ≐ g(X, X, f(X)) [Z/X]
g(Z, Z, f(Z)) ≐ g(Z, Z, f(Z)) ✓
→ mgu([Z/Y], [Z/X]).
Hier also konsequent von links nach rechts auf der linken Seite. Oder dürfte ich auch von rechts nach links gehen?
g(X, X, f(Z)) ≐ g(Y, X, f(X)) [Z/X]
g(Z, Z, f(Z)) ≐ g(Y, Z, f(Z)) [Z/Y]
g(Z, Z, f(Z)) ≐ g(Z, Z, f(Z)) ✓
→ mgu([Z/X], [Z/Y]).
Oder gar auf der rechten Seite anfangen?
g(X, X, f(Z)) ≐ g(Y, X, f(X)) [X/Z]
g(X, X, f(X)) ≐ g(Y, X, f(X)) [Y/X]
g(Y, Y, f(Y)) ≐ g(Y, Y, f(Y)) ✓
→ mgu([Y/Z], [Y/X]).
Da man die Variablen quasi beliebig umgebennen kann, kommt hier immer dasselbe raus.
Nur gibts eine Richtlinie?
Wenn du den Algorithmus von Robinson anwendest, musst du links anfangen
Sprich zuerst [X/Y]
[Y/X] geht vermutlich auch, da die Unifikation ja kommutativ ist.
Ansich ist mir aber nicht ganz klar, welcher der “Algorithmus aus der Vorlesung” ist.
Schließlich haben wir zum einen den Robinson-Algorithmus, als auch den mit der Mengenschreibweise
Bsp.
g(X,X, f(Z)) = g(Y,X,f(X))
{X = Y, X = X, f(Z) = f(X)}
{X = Y, X = X, Z = X}
{X = Y, X = X, X = Z}
besprochen