Unifikation

Neue Frage »

Auf diesen Beitrag antworten »
Alex Unifikation

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
 
Auf diesen Beitrag antworten »
Karlito

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] 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
Auf diesen Beitrag antworten »
Alex

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
Auf diesen Beitrag antworten »
Karlito

Passt. Darauf komm ich auch.

VG,

Karlito
 
Auf diesen Beitrag antworten »
Alex

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
Auf diesen Beitrag antworten »
Karlito

Kann nicht nachvollziehen, ob dein Weg richtig ist, aber ich komme auch auf "nicht unifizierbar".

VG,

Karlito
Auf diesen Beitrag antworten »
Alex

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
Auf diesen Beitrag antworten »
Karlito

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
Auf diesen Beitrag antworten »
Alex

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
Auf diesen Beitrag antworten »
Karlito

Hallo,

prinzipiell richtig Unifiziert, nur eine Regel vergessen:

Zitat:
Original von Alex
Y/h(X,Y)


Da liegt dein Fehler...

VG,

Karlito
 
Neue Frage »
Antworten »


Verwandte Themen

Die Beliebtesten »
Die Größten »
Die Neuesten »