darf man , unter Regeln und aus Kommentar von tannenbaum Lsg. Ansatz zur Altklausur Aufgabe 4 von WS1617 - Grundlagen der Logik in der Informatik - FSI Informatik Forum) Ersetze Variable durch Konstante
3b) Ersetze Variable durch eine andere Variable
3c) Ersetze Variable durch Funktion einer Variablen
Hier ist mir noch aufgefallen, dass du jede mehrmals vorkommende Variable umbenennst. Du bennest allerdings nur die ungebundenen, also freien Variablen um! In dieser Aufgabe sind alle Variablen gebunden, daher musst du sie nicht umbennen.
die Lösung sind nicht aktuelle!!! habe ich in einer Thread wieder aktualisiert!!!
Ich kram das mal hervor, den ich verssteh nicht warum bei Substitution „2 + 3“ der mgu=f(x)/x . rauskommt, ich darf doch bei einer unifikation keine x = f(x) haben, das wäre doch occurs und somit bottom… kann mir jemand erklären ob das tatsächlich falsch ist, oder darf man das hier tatsächlich machen, und wenn ja warum?
Edit: ok hat das was mit disjunkter variablenmenge zu tun? also müste man einfach(wenn man das darf???) z.B. in Klausel 3 -P(x) in -P(x’) umbennen? dann wäre der mgu ja [f(x)/x’] ?
Exakt! Vor jeder (!) Anwendung der Resolutionsregel musst du die Variablenmengen beider zu resolvierender Klauseln disjunkt machen. Das steht im Skript direkt unter der „RIF“-Regel in Kapitel 8.
Ich glaube, ich hab das damals von der Notation her so gemacht: {R(x, f(x))} = {R(x’), f(x’))} und dann bei der Resolution mit einer anderen Klausel den Pfeil von der rechten Seite der Gleichung gezogen.
So wie ich das gerade sehe, fehlt die Disjunktheit in allen Schritten der obigen Lösung.