Wenn man zB. hat:
{A}{B}{A v C}{-B}{C ^ D}{D}{G} muss man alle klauseln benutzen?
kann man nicht B und -B resolvieren und kommt dann sofort auf leere klausel -> Formel nicht erfüllbar?
Richtig, es müssen nicht alle Klauseln benutzt werden.. bei der Resolution verwendet man zwar die Mengendarstellung, die Formel selbst liegt ja aber in KNF vor; alles Konjunktionen. Damit die Formal wahr wird, muss also jede Klausel wahr sein… kannst du irgendwie die leere Klausel ableiten, sind andere (ggf. unbenutzte Klauseln) nicht mehr von Interesse, dann dann hast du gezeigt dass die Formel unerfüllbar ist.
Greetz
Kann man denn auch Klauseln mehrfach benutzen zum resolviern?
Also wenn man zwei Klauseln zusammen resolviert, dann darf man nur das, was dabei rauskommt zur weiteren Resolution mit anderen Klauseln weiterverwenden.
In deinem Beispiel dürftest Du dann
{B} und {-B} jeweils nicht weiter benutzen, falls Du sie schon zusammen resolviert hast. Nur die daraus resultierende leere Klausel dürftest du noch benutzen.
Deswegen sollte man sich am Anfang überlegen, welche Resolutionsreihenfolge am wenigsten Schritte erfordert.
EDIT :
Das mehrfache Benutzen ist glaub ich nicht streng verboten, ist aber redundant und nicht wünschenswert, da es dann kein klarer eindeutiger Resolutionsweg mehr ist.
nun ja, es kann aber von vorteil sein: sagen wir ich habe ein einzelnes literal durch resolution zweier klauseln erhalten. dann kann ich damit das komplementäre literal in allen anderen klauseln herauslöschen.. vielleicht kommt das oft vor, dann ist es doch in ordnung, die selbe klausel (mein einzelnes literal) auch oft als resolutionsklausel zu verwenden..
Ja okay, das kann ich mir auch vorstellen.
Also man darf ein Literal durchaus öfter benutzen. Siehe dazu F1 Skript Vorlesung Nummer 8 Folie 31 z.B.
