Resolution erklären

Neue Frage »

donvito Auf diesen Beitrag antworten »
Resolution erklären
Edit: Bitte Verschieben, habe das hier wohl falsch abgeheftet Big Laugh

Hallo,

kann mir bitte mal jemand erklären, wie der Resolutionsalgorithmus funktioniert?
Ich habe es soweit verstanden:
1. KNF bilden.
2. Klauseln miteinander vergleichen und Resolvente bilden.

Doch mein Problem ist jetzt: Manchmal gibt es mehrere Möglichkeiten die Resolvente zu bilden. Dann darf man ja jeweils nur eine Variable rausstreichen. Demnach ist die Resolution nicht eindeutig?
Und die wichtigste FRage: Mit was vergleiche ich nun im dritten, vierten, usw. Schritt die vorhandenen Resolventen?

Das ganze ist dann vorbei, wenn ich eine leere Menge erhalte. Geht das nur, indem ich zwei Klauseln, z.B. habe, ober entsteht die leere MEnge auch, wenn ich einfach garnichts mehr machen kann. DAs kann ja z.B. sein, wenn alle Literale positiv sind.

Hier mal meine Aufgabe:
Mazze Auf diesen Beitrag antworten »

Zitat:
Doch mein Problem ist jetzt: Manchmal gibt es mehrere Möglichkeiten die Resolvente zu bilden. Dann darf man ja jeweils nur eine Variable rausstreichen. Demnach ist die Resolution nicht eindeutig?


Das Ergebnis der Resolution ist eindeutig, aber zum Beispiel gibt es bei



zwei mögliche Resolventen.

Zitat:
Und die wichtigste FRage: Mit was vergleiche ich nun im dritten, vierten, usw. Schritt die vorhandenen Resolventen?


Du kannst jede Resolvente in deine Formelmenge aufnehmen und benutzen, um neue Resolventen zu bekommen.

Zitat:
ober entsteht die leere MEnge auch, wenn ich einfach garnichts mehr machen kann


Bei endlicher Formelmenge gibt es endlich viele Resolventen. Wenn die leere Menge nicht dabei ist, so folgt entsprechende Aussage nicht.
donvito Auf diesen Beitrag antworten »

Danke für deine Antwort!

Formelmenge = ursprüngliche Klauselmenge + alle Resolventen?

Das heißt ich probiere da einfach ein bisschen rum und wenn nicht irgendwann entweder eine leere Menge auftritt oder ich eben nichts mehr machen kann, bin ich fertig?
Tobias Auf diesen Beitrag antworten »

Hast du verstanden wofür man Resolution verwendet und warum sie korrekt und vollständig ist?
donvito Auf diesen Beitrag antworten »

Um zu zeigen, dass eine Formel erfüllbar ist.

Die Beweise muss ich mir wohl nochmal ansehen, sind aber auch nicht so wichtig für die Klausur in Künstliche Intelligenz ;-)
Tobias Auf diesen Beitrag antworten »

Zitat:
Um zu zeigen, dass eine Formel erfüllbar ist.

Wie macht man das?
 
 
donvito Auf diesen Beitrag antworten »

Ich zeige durch Resolution, dass die Formel unerfüllbar ist. Das heißt wenn ich die leere Menge von der ursprünglichen Formel ableiten kann. Dann ist die Formel unerfüllbar. Denn das hieße dann ja, dass eine Klausel nicht erfüllt werden kann. Somit ist die gesamte Formel nicht erfüllbar. Ansonsten endet der Algorithmus mit dem Ergebnis erfüllbar, wenn "man nichts mehr machen kann".

Edit: Frage: Was passiert, wenn ich {B, C, -C} mit {A, C} vergleiche? Fällt das C dann ganz weg oder bleibt da eins übrig?
Außerdem ist mir immer noch nicht ganz klar, in welcher Reihenfolge ich was mit wem vergleichen muss.
Neue Frage »
Antworten »



Verwandte Themen

Die Beliebtesten »
Die Größten »
Die Neuesten »