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.
SLD-Resultion
Könnte uns jemand bitte erklären, wie die SLD-Resolution nochmal funktioniert?
Beispielsweise an der Präsenzaufgabe Blatt 7, Aufgabe 2:
← append([0|X],[1|Y],[0,1|Z])
Wir haben die Resolution mal mit der zweitschnellsten Anfrage von Blatt 7 Aufgabe 2 versucht.
Aktualisiert nach mnschmits Anmerkungen.
<-- append ( [0|X], [1|Y], [0, 1, Z] )
Rcons mit append ( [X0 | Y0], Z0, [X0 | W0] )
mgu1 = [X0 -> 0, X -> Y0, Z0 -> [1|Y], W0 -> [1|Z] ]
<-- append ( Y0, [1|Y], [1|Z] )
Rcons mit append ( [[X1 | Y1], Z1, [X1|W1] )
mgu2 = [X1 -> 1, Y0 -> [1|Y1], X1 -> 1, Z -> W1 ]
<-- append ( Y1, [1|Y], W1]
Rnil mit append ( [], List, List)
mgu3 = [Y1 -> [], List -> [1|Y], W1 -> [1|Y] ]Rückwärtseinsetzen der Unifikatoren:
mgu3 in mgu2: [W1 -> [1|Y], X1 -> 1, Y0 -> [1|[]], Y1 -> [], Z -> [1|Y], Z1 -> [1|Y], List -> [1|Y] ]
mgu2 in mgu1: [W0 -> [1|[1|Y]], W1 -> [1|Y], X -> [1|[]], X0 -> 0, X1 -> 1, Y0 -> [1|[]], Y1 -> [], Z -> [1|Y], Z0 -> [1|Y], Z1 -> [1|Y], List -> [1|Y] ]Antwort ist dann [m][ X → [1|[]], Z → [1|Y] ][/m]
Stimmt das so?
Hab leider keine Zeit, mir das anzuschauen, aber einen Tip: Schaut euch an, wie Prolog die Anfrage beantwortet.
$ swipl
?- trace.
[trace] ?- append([0|X],[1|Y],[0,1,Z]).
(Ach ja, ihr wollt da euer eigenes append verwenden, sonst spuckt trace nichts aus)
Sieht meiner Meinung nach recht richtig aus. Ein paar Anmerkungen:
der mgu2 ist etwas komisch. Ein unmotiviertes [X1,W1] fliegt am Schluss rum und es fehlen Z → W1, sowie Z1 → [1|Y].
Vorsicht bei eurem “Rückwärtseinsetzen”: es müssten am Schluss alle Ersetzungen in einer einzigen Substitution enthalten sein, da ihr alle eure gefundenen mgus zusammenfassen wollt.
Übrigens ist Rcons eher append([X|Y], Z, [X|W]) ← append(Y, Z, W).
Ist euch der Unterschied zwischen , und | bei Listen in Prolog bekannt?
Danke für die Bestätigung.
Oh richtig, bin beim Abtippen in der Zeile verrutscht.
Tippfehler. [ Head | Tail ] und [ Elem1, Elem2 ] ist der Unterschied.
Werde das Beispiel oben korrigieren.
Danke für deine Antwort!
Aber was ist das „Rückwärtseinsetzten“ jetzt genau? Im (inoffiziellen) Skript steht einfach nur „Einsetzten der zweiten in die erste Substitution“. Das würde in diesem Fall, imho, aber nicht zu der Antwort führen, die Prolog gibt, denn dann würde es eine Subsitution [W0 → [1|[1|Y]] geben und keine mit Z.
Wenn man etwas googlet trifft man auf Quellen von anderen Unis, die nicht von „Rückwärtseinsetzen“ sprechen sondern von „Komposition“, also Rückwärts anwenden und Vereinigen. Damit würde es funktionieren, denn die benötigte Substitution [Z-> [1|y]] würde es dann auch in dem ersten/letzten mgu geben.
Ich schließe daraus, dass wir dann die Substiutionen Rückwärtseinsetzen und Zusammenführen müssen. Stimmt das?
Vielen Dank!