Auf der FGI1-Seite gibts ja alte Klausuraufgaben, ich stell hier mal meine Lösung für das erste Blatt rein - wär super, wenn das jemand mit seiner Lösung abgleichen könnte.

Logik (Blatt1):


[img]http://mokrates.de/cgi-bin/texstring?1.%20((%20%5Cneg%20P%20%5Cvee%20%5Cneg%20Q%20)%20%5Crightarrow%20(%20R%20%5Cvee%20S))%20%5Cwedge%20(%20%5Cneg(%20%5Cneg%20P%20%5Cvee%20Q))%0A%0A%0AKNF:%20(%5Cneg%20P%20%5Cvee%20%5Cneg%20Q%20%5Cvee%20R%20%5Cvee%20S)%20%5Cwedge%20(%5Cneg%20P%20%5Cvee%20%5Cneg%20Q%20%5Cvee%20R%20%5Cvee%20%5Cneg%20S)%20%5Cwedge%20(%5Cneg%20P%20%5Cvee%20%5Cneg%20Q%20%5Cvee%20%5Cneg%20R%20%5Cvee%20S)%20%5Cwedge%20(%5Cneg%20P%20%5Cvee%20%5Cneg%20Q%20%5Cvee%20%5Cneg%20R%20%5Cvee%20%5Cneg%20S)%20%0A%0A%0A2.%20(Q%20%5Cleftrightarrow%20R)%20%5Cwedge%20%5Cneg%20S%0A%0ADNF:%20(%5Cneg%20Q%20%5Cwedge%20%5Cneg%20R%20%5Cwedge%20%5Cneg%20S)%20%5Cvee%20(Q%20%5Cwedge%20R%20%5Cwedge%20%5Cneg%20S)[/img]

Ich hab hier nur einmal die KNF und einmal die DNF angegeben, die beiden fehlenden waren mir doch zu lang fürs Abtippen, aber daran sollte ja klar werden, ob der Weg richtig war/ist, oder auch nicht.

Ganz vergessen die Lösung zur unifizierbaren Menge mit einzutippen:

Sie ist nicht unifizierbar, da u sowohl durch b, als auch durch f(b) ersetzt werden müsste.

Ich bin an der Stelle durch anwendung des UniAlgo auf folgendes gekommen.


o1[x/g(y,z)]
o2[u/f(y)]

dann sind die ersten beiden gleich, mit dem letzten kann man es nicht mehr unifizieren, da keine variablen mehr vorhanden sind die man substituieren koennte und R(g(u,a),(f(b)) != R(g(y,z),f(z))

Den ersten Schritt teile ich, aber bevor du dazu kommst, u und f(y) zu unifizieren, musst du erst noch gucken, was mit z/a ist, da du ja von links nach rechts vorgehst. Ok, da müsste man sogar noch y/u einbeziehen, oder?
Ich komme jedenfalls auch soweit, dass die ersten beiden übereinstimmen, aber das letzte nicht. Somit ist die Menge doch nicht unifizierbar, oder?!

Gut das du es sagst, ich korrigiere mich.

o1[x/g(y,z)]
o2[u/f(y)]

wuerde ich weiterhin behaupten. Ich verstehe den Unifikationsalgorithmus so, dass man den ersten Unterschied zwischen zwei, Praedikaten sucht und dann wieder von vorne beginnt. Wobei, dass vorne beginnen nicht so deutlich drinne steht wie ich finde.

Ich wuerde also zu erst die ersten beiden Praedikate unifizieren und mich dann, an das Dritte machen.

Ich wuerde also Sagen, dass da nun steht
{ R(g(y,z),f(z)) , R(g(f(y),a),(f(b)) } //das u durch f(y) ersetzt wird hab ich vorher auch uebersehen

Der naechste Schritt waere dann in meinen Augen
o3[y/f(y)] hier bricht der Unifikationsalgorithmus ab, da y als echter Term in f(y) vorhanden ist.