 Unifikation |
Alex
Mitglied
Dabei seit: 22.02.2012
Beiträge: 28
 |
|
Hallo,
ich habe die Folgenden Termpaare Unifiziert, aber ich weiß nicht genau ob sie richtig sind.
Gegeben:
U1= f(X, g(a,h(Y,a), f(a,X,Z)), Y)
U2= f(X, g(a, X , f(a,X,Y)), h(Z,Z))
U3= f(X, g(a, X , f(a,X,Y)), h(X,Y))
Meine Lösung:
U12= X/ h(Y,a) , Y/Z , Y/h(Z,Z)
U12= f(h(Y,a), g(a,h(h(Z,Z), a), f(a,h(Y,a),Z))
U13= X/h(Y,a) , Y/Z , Y/h(X,Y)
U13= f(h(Y,a), g(a,h(X,Y),a) , f(a,h(Y,a), h(X,Y)), h(X,Y))
Gruß Alex
Dieser Beitrag wurde 1 mal editiert, zum letzten Mal von Alex: 28.08.2012 23:21.
|
|
28.08.2012 23:20 |
|
|
Karlito 
Kaiser
Dabei seit: 11.04.2011
Beiträge: 1.461
|
|
Hallo,
entschuldige bitte die sehr späte Antwort. Soweit ich mich nicht verrechnet habe, sind beide Lösungen falsch.
Zu U12: Kann es eine Substitution ![[latex]\sigma = \{Y\mapsto Z, Y\mapsto h(Z,Z)\}[/latex]](http://www.matheboard.de/latex2png/latex2png.php?\sigma = \{Y\mapsto Z, Y\mapsto h(Z,Z)\}) geben? Auch so würde ich meinen, dass die Ableitung falsch ist.
Schreib doch mal bitte zu beiden Problemen, wie du den Unifikationsalgorithmus angewendet hast (im Kopf kann ich nicht empfehlen, das geht meist schief).
VG,
Karlito
|
|
|
31.08.2012 12:17 |
|
|
Alex
Mitglied
Dabei seit: 22.02.2012
Beiträge: 28
|
|
Hallo,
vielen dank für deine Antwort Karlito.
Ich habe es nochmal gerechnet, und das kam heraus:
U12:
f(h(h(Z,Z),a),g(a,h(h(Z,Z),a), f(a,h(h(Z,Z),a),Z)), h(Z,Z))
Gruß Alex
|
|
|
17.09.2012 22:04 |
|
|
Karlito
Kaiser
Dabei seit: 11.04.2011
Beiträge: 1.461
|
|
Passt. Darauf komm ich auch.
VG,
Karlito
|
|
|
17.09.2012 22:13 |
|
|
Alex
Mitglied
Dabei seit: 22.02.2012
Beiträge: 28
|
|
Hallo,
ich habe noch eine Frage zu diesen Aufgabe:
A1= f(U, g(a,h(V,a), f(a,U,W)), V )
A2= f(X, g(a, X , f(a,X, Y)), h(X,Y))
X/U X/h(V,a) Y/W V/h(X,Y)
ich komme hier auf keinem Ergebnis, wegen Unvereinbarkeit von X.
Stimmt das so.
Gruß Alex
|
|
|
20.09.2012 10:58 |
|
|
Karlito
Kaiser
Dabei seit: 11.04.2011
Beiträge: 1.461
|
|
Kann nicht nachvollziehen, ob dein Weg richtig ist, aber ich komme auch auf "nicht unifizierbar".
VG,
Karlito
|
|
|
20.09.2012 11:18 |
|
|
Alex
Mitglied
Dabei seit: 22.02.2012
Beiträge: 28
|
|
Vielen Dank für deine Hilfe Karlito.
Ich habe noch eine Theorie Frage bei dem ich nicht weiter komme.
Wann ist die Unifikation zur Auswertung eine logischen Programmes von Beduetung, wenn dieses
- nur Aussagenvariablen enthält (und keine Prädikatensymbole)
- unter anderem Prädikatensymbole ?
Ich weiß das Unifkation verwendet wird zur Parameterübergabe in Prolog um SLD Anfragen zu lösen.
Kannst du mir dabei weiterhelfen?
Gruß Alex
|
|
|
20.09.2012 13:45 |
|
|
Karlito
Kaiser
Dabei seit: 11.04.2011
Beiträge: 1.461
|
|
Hi,
ich kann dir nur sagen, dass es bei der Prädikatenlogik bei Resolutionsbeweisen notwendig ist. SLD ist eine spezialform von Resolutionsbeweisen.
In der Aussagenlogik fällt mir nichts ein. Denke da ist keine Unifikation nötig ist.
VG,
Karlito
|
|
|
20.09.2012 14:11 |
|
|
Alex
Mitglied
Dabei seit: 22.02.2012
Beiträge: 28
|
|
Hallo,
ich habe noch eine frage zu der Aufgabe U13: Ist das richtig Unifiziert?
X/h(Y,a)
Y/Z
Y/h(X,Y)
f(h(Y,a), g(a,h(Y,a), f(a,h(Y,a) , Z)) , h(X,Y))
f(h(Y,a), g(a,h(Y,a), f(a,h(Y,a),h(X,Y)), h(X,Y))
Z/h(X,Y)
f(h(Y,a), g(a,h(Y,a), f(a,h(Y,a) , h(X,Y)) , h(X,Y))
f(h(Y,a), g(a,h(Y,a), f(a,h(Y,a), h(X,Y)), h(X,Y))
Gruß Alex
|
|
|
08.10.2012 20:29 |
|
|
Karlito
Kaiser
Dabei seit: 11.04.2011
Beiträge: 1.461
|
|
Hallo,
prinzipiell richtig Unifiziert, nur eine Regel vergessen:
| Zitat: |
Original von Alex
Y/h(X,Y)
|
Da liegt dein Fehler...
VG,
Karlito
|
|
|
10.10.2012 09:35 |
|
|
|
