Probeklausur A4 Resolutionsverfahren

[system]

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.

[momo8]

Probeklausur A4 Resolutionsverfahren

1. ¬R(x,y),¬R(y,z),R(x,z) 2. R(x,f(g(x))) 3.R(f(x),a) 4.¬R(c,a)

1+2, mgu=[f(g(x))/y]
5. ¬R(fg(x)),z),R(x,z)

5+3: mgu=[g(x)/x,a/z]
6. R(g(x),a)

6+4: mgu=[c/g(x)] unerfüllbar
eine Frage , darf man eigentlich eine Konstante die Funktionssymbol einzusetzen???,

[FloH]

---

Ich würde deine letzten zwei Schritte tauschen. Du versuchst am Ende eine Funktion durch eine Konstante zu ersetzen.
Wenn du z.B. x durch eine Konstante substituierst, dann steht die Konstante auch in der Funktion, sofern ich deine Frage richtig verstanden hab.

1. ¬R(x,y), ¬R(y, z),R(x, z) 2. R(x, f(g(x))) 3.R(f(x), a) 4.¬R(c, a)

1+2 mgu = [y-> (f(g(x))]
5. ¬R(f(g(x)), z), R(x, z)

4+5 mgu = [z → a, x → c]
6. ¬R(f(g(c)), a)

6+3 mgu = [x → g(c)]
7. { }

[momo8]

---

@FloH

Ich würde deine letzten zwei Schritte tauschen. Du versuchst am Ende eine Funktion durch eine Konstante zu ersetzen.
Wenn du z.B. x durch eine Konstante substituierst, dann steht die Konstante auch in der Funktion, sofern ich deine Frage richtig verstanden hab.

1. ¬R(x,y), ¬R(y, z),R(x, z) 2. R(x, f(g(x))) 3.R(f(x), a) 4.¬R(c, a)

1+2 mgu = [y-> (f(g(x))]
5. ¬R(f(g(x)), z), R(x, z)

4+5 mgu = [z → a, x → c]
6. ¬R(f(g(c)), a)

6+3 mgu = [x → g(c)]
7. { }

ich werde zustimmen, es macht schon mehr sinn und auch schon logisch! g(c) ist auch eine Konstante, eine Konstante kann die Variable beliebig einzusetzen!