Was meint man genau mit "mittels der Resolutionsmethode"?
Meint man damit einfach die Resolutionsregel wie immer, oder steckt da noch mehr hinter?
Wenn man das Ergbenis umformt dann erhält man die Formel:
(A und B und NegC und NegD)
Meiner Meinung nach kann man so etwas gar nicht kommen, denn dann müssten wir ja 4 verschiedene Enden haben.
Ist es überhaupt ratsam die Formel so umzuformen?
für die Zukunft: möglichst in den bereits vorhandenen Thread zu Blatt 9 Aufgabe 2 posten..,
obs in der aktuellen Vorlesung eine besondere "Resolutionsmethode" gibt, wer weiss,
sonst normale Resolution
das mit den 4 Enden versteh ich nicht,
ist doch ne einwandfreie KNF?,
ratsam ist es allerdings nicht [img]
http://www.fb18.de/gfx/25.gif[/img], das stimmt schon
ratsam ist es allerdings nicht , das stimmt schon
Aber das Ergebnis einer Resultion ist doch immer eine Disjunktion auf Literalen. Wie kann so eine Disjunktion von Literalen äquivalent zu einer Konjunktion von Literalen(A und B und -C und -D) sein.
Denn die Umformung ist ja meiner Meinung nach korrekt!?
Bedeutet das also ich muss eine Resultion solange anwenden bis einmal nur A , einmal nur B, einmal bis nur -C und einmal bis nur -D übrig bleibt !?
versteh immer noch nicht die Frage,
was ist das Ergebnis einer Resolution?
Resolution wird auf eine Konjunktion von Klauseln angewendet,
dabei entstehen neue Klauseln,
also von mir aus ist das Ergebnis dann die bisherigen Klauseln + die neuen,
das macht wieder eine Konjunktion von Klauseln
(Klauseln sind Disjunktionen von Literalen)
du musst die Resolution so lange anwenden bis die leere Klausel rauskommt,
als Zwischenschritte können durchaus A oder B oder was auch immer für Klauseln rauskommen,
edit
(A und B und NegC und NegD)
sind vier verschiedene Klauseln und nicht eine, falls du das denkst
aber das stört ja auch nicht
Aufgabenstellung:
Zeigen mittels der Resultionsmethode, dass -((A*B)->(C+D)) ein Folgerung aus der Formelmenge M sind
Wobei ((A*B->(C+D)) = A*B*(-C)*(-D) ist.
Wie geht man jetzt ganz allgemein vor wenn man mit Hilfe der Resultion so eine Konjunktion von literalen folgern will!?
Bis jetzt haben wir die Resulotion nämlich nur verwendet um die Unerfüllbarkeit zu prüfen!
das ist ja auch der Trick weswegen ich geschrieben habe
ratsam ist es allerdings nicht , das stimmt schon
du musst dir eine Formel überlegen, die, wenn unerfüllbar, beweist, dass die Behauptung richtig ist,
meistens geht sowas mit Umkehrung..
"beweise dass F allgemeingültig ist"
-> zeige dass -F unerfüllbar ist
wie resolviere ich denn in einer formelmenge`?
muss man die junktoren erts so umbasteln, dass alle zB in knf ist?
Resolution funktioniert nur in KNF, richtig
also die Formel erst mal dahingehend umformen,
HMmm…
Irgendwie verstehe ich nun nicht wohin meine Resolution so führen soll…? Zur leeren menge? da finde ich irgendwie grad keinen weg. Gibt es vllt ncoh einen kleinen Denkanstsoss der mir helfen könnte?
Slater hat doch schon ein guten Tip gegeben!;) Mir hat er jedenfalls geholfen! Schau ein paar Zeilen oben nach!
Ja, mit hilfe von google hab ich nun glaub ich gefunden was ich noch brauchte…
