Hallo, habe einige Fragen zur Resolution.

Warum muss man nicht alle komplementären Literale aus der Formelmenge entfernen, bzw. welche kann ich ignorieren?

Wenn der Resolvent nicht die leere Menge ist, weiß ich dann genau, dass die Formel oder Formelmenge immer erfüllbar ist?

Danke, Gruß Jan

Wenn der Resolvent nicht die leere Menge ist, weiß ich dann genau, dass die Formel oder Formelmenge immer erfüllbar ist?

Der Resolutionssatz besagt:

Eine Klauselmenge F ist unerfüllbar genau dann wenn die leere Klausel Element ist aus Res^*(F), d.h. wenn die leere Klausel aus F (mit wieviel Schritten auch immer, daher der Stern), resolvierbar ist.

Wenn du die leere Klausel also nicht resolvieren kannst, dann ist die Formelmenge folglich erfüllbar (wäre sie nämlich doch unerfüllbar steht das im Widerspruch zu obigem Satz). Man muss aber darauf aufpassen, dass man um diese Aussage treffen zu können wirklich alle Resolventen bilden muss, d.h. man muss Res^1(F), Res^2(F), Res^3(F),…. bilden bis man einen Indize k findet mit Res^k(F) = Res^(k+1)(F). Dann kommt nämlich keine neue Resolvente dazu und dann ist eben auch Res^*(F) = Res^k(F).

Hoff' es hilft [img]http://www.fb18.de/gfx/23.gif[/img]

Cheers,
Frank

P.S. Deine erste Frage verstehe ich leider nicht, kannst du nochmal genau beschreiben, was du meinst und machen möchtest?

Hallo Azure,
erst mal besten Dank.

2 Prüfungsfragen waren:
1. "Kann eine Klausel {A, nichtA} bei einer Resolution ignoriert werden?"

2. "Wenn in einer Klauselmenge die atomare Fromel A immer nur in der Form nichtA vorkommt, können dann die Klauseln, die diese nichtA's enthalten, ignoriert werden?"

Gruß Jan

1. "Kann eine Klausel {A, nichtA} bei einer Resolution ignoriert werden?"

Ja.
Begründung 1: Da die Klausel tautologisch ist, kann sie nichts dazu beitragen, eine Unerfüllbarkeit nachzuweisen. Das ist aber das Ziel der Resolution.
Begründung 2: Die einzigen Klauseln, die man mit {A, !A} resolvieren könnte, wären {A} = {A, A} und {!A} = {!A, !A}. Bei der Resolution kommt dann aber genau diese Klausel wieder heraus, man gewinnt also nichts.

2. "Wenn in einer Klauselmenge die atomare Fromel A immer nur in der Form nichtA vorkommt, können dann die Klauseln, die diese nichtA's enthalten, ignoriert werden?"

Ziel der Resolution ist es, irgendwie auf die leere Formelmenge zu kommen. Wenn man dazu die Formeln mit !A benutzt, muss man also irgendwie das !A entfernen. Das geht aber nur, indem man das komplementäre Literal A benutzt. Hat man dieses nicht zur Verfügung, kann man das !A nicht entfernen. Es bringt einem also nichts, wenn man Formelmengen, die !A enthalten, zur Resolution benutzt, man kann diese also ignorieren.

Vielen Dank,
dass hat für's Verständnis echt weitergeholfen.
Danke, Gruß Jan