Informatiker Board (http://www.informatikerboard.de/board/index.php)
- Themengebiete (http://www.informatikerboard.de/board/board.php?boardid=1)
--- Theoretische Informatik (http://www.informatikerboard.de/board/board.php?boardid=5)
---- Logik (http://www.informatikerboard.de/board/board.php?boardid=16)
----- Unifikation (http://www.informatikerboard.de/board/thread.php?threadid=1268)


Geschrieben von Alex am 28.08.2012 um 23:20:

  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



Geschrieben von Karlito am 31.08.2012 um 12:17:

 

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



Geschrieben von Alex am 17.09.2012 um 22:04:

 

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



Geschrieben von Karlito am 17.09.2012 um 22:13:

 

Passt. Darauf komm ich auch.

VG,

Karlito



Geschrieben von Alex am 20.09.2012 um 10:58:

 

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



Geschrieben von Karlito am 20.09.2012 um 11:18:

 

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

VG,

Karlito



Geschrieben von Alex am 20.09.2012 um 13:45:

 

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



Geschrieben von Karlito am 20.09.2012 um 14:11:

 

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



Geschrieben von Alex am 08.10.2012 um 20:29:

 

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



Geschrieben von Karlito am 10.10.2012 um 09:35:

 

Hallo,

prinzipiell richtig Unifiziert, nur eine Regel vergessen:

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


Da liegt dein Fehler...

VG,

Karlito


Forensoftware: Burning Board, entwickelt von WoltLab GmbH