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.
Orient
Eine Frage zum Orient:
Im folgenden habe ich je einen Ausschnitt zu zwei alten, richtig gelösten Übungsaufgabe. Man hat folgende Literale:
A)
- z = e, z * i(z) = y
- z = e, y = z * i(z)
- z = e, y = e * i(e)
B)
- i(z*i(x)) = y, y = i(x)
- y = i(z*i(x)), y = i(x)
- i(x) = i(z * i(x)) , y = i(x)
Von 1. auf 2. wurden in beiden Fällen Orient ausgeführt, von 2. auf 3. elim. In A hat bringt man die in elim zu ersetzende Terme auf unterschiedliche Seiten, in B auf die gleiche Seite. Kann jemand erklären, warum man in beiden Fällen ein orient braucht bzw. warum es vor dem elim ausgeführt werden muss/musste?
Du hättest bei A) und B) jeweils den orient und elim Schritt vertauschen können. Du musst nur bei elim beachten, dass die Variable auf der linken Seite der Gleichung stehen muss (per Konvention). Bei dem Unifikationsalgorithmus brauchst du dir sowieso keine Gedanken machen, jeder Schritt führt dich garantiert näher zur Lösung, siehe Terminationsbeweis im Skript. Eventuell könntest du durch geschicktes Hinsehen hier und dort Schreibarbeit sparen (lange Terme erst am Ende per elim ersetzen), aber ob sich das bei den Aufgaben in der Klausur lohnt, ist fraglich 
1 „Gefällt mir“