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.
Terminiert die Resolution wirklich immer bei der minimalen Klauselmenge?
Hallo zusammen,
ich beschäftige mich gerade mit dem Resolutionsalgorithmus aus der Vorlesung. Mir leuchtet die Funktionsweise davon auch ein. Mir ist aber aufgefallen, dass manchmal der Algorithmus nicht ganz bis zum Ende “resolviert” (also nicht zur minimalen Klauselmenge) abhängig davon mir welchen Anfangsklauseln man begonnen hat. Gibt es da einen sinnvollen Trick, wie man am schnellsten zur minimalen Klauselmenge kommt?
Also ich meine Ziel ist ja zB die leere Menge herzuleiten. Gibt es einen Trick, wie man sicher und am schnellsten auf die leere Klausuelmenge kommt? Manchmal habe ich das Gefühl, dass es manchmal nicht terminiert. Muss ich dann alle Möglichkeiten durchprobieren?
Vielen Dank!
froschigon
Meinst du den Algorithmus für FOL oder Aussagenlogik? Bei FOL terminiert der Algorithmus ja eventuell nicht, bei Aussagenlogik immer egal mit was du anfängst.
Ja, ich meinte den Algo der FOL. Wenn man jede Klausel mit jeder resolviert hat, und es in der Klausur nicht terminiert, muss an wohl einfach hinschreiben, dass es scheinbar keine Lösung gibt? Kann sowas dran kommen?
Wenn man Klauseln mit Variablen hast kann man ja immer weiter resolvieren, indem man andere Subsitutionen wählt. In dem Fall das es nicht terminiert hast du entweder falsche Substitutionen gewählt oder es gibt wirklich keine Lösung.
Das bedeutet, dass die Formel erfüllbar war. Wenn ich das Skript richtig lese, dann terminiert die Resolution in der Tat für erfüllbare Formeln. (Da du aber meist die Gültigkeit zeigen willst, also die Unerfüllbarkeit der Negation, hast du dabei keine zwingende Termination.)
Ich vermute, es gibt nur endlich viele MGUs zwischen zwei Klauseln.
Im Skript steht, dass die Resolution für unerfüllbare Formeln terminiert und für erfüllbare eventuell nicht:
Laut Skript gibt es sogar eigentlich nur einen, die Resolution terminiert aber trotzdem nicht immer.
Stimmt, du hast Recht! (Das beinhaltet also keine Negation, bezieht sich nur auf die reine Resolution. Das war das, was mich verwirrt hat ;))
[quote=Jonas S]Laut Skript gibt es sogar eigentlich nur einen, die Resolution terminiert aber trotzdem nicht immer.
[/quote]
Es gibt mehrere, sie sind jedoch identisch bis auf bijektive Umbenennungen.
Dem stimme ich nicht ganz zu. Klar, wenn du die Resolventen mit einbeziehst, dann kannst du u. U. wieder endlos resolvieren. Aber bei zwei festen Klauseln kannst du nur endlich viele Substitutionen und damit Resolventen herausbekommen. Es gibt auf der endlichen Menge an freien Variablen auch nur endlich viele bijektive Umbenennungen.
Ich meinte wenn man mit den Resolventen weitermachst, sonst hast du recht.