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.
unit propagation (UP) und pure literal elimination (PLE)
Ich habe noch Fragen zu UP und PLE.
Wir haben in der Übung zu jedem folgendes Beispiel genannt bekommen:
PLE:
{b} {a , b} {c, a’} = {c, a’} => d.h. man löscht alle Klauseln in den ein b vorkommt und dann kommt bei der Resolution das gleiche raus wie vor PLE.
Hier hätte ich aber folgendes Gegenbeispiel:
{b} {a , b} {c} {c’} = “leer” (nach PLE) - das macht aber keinen Sinn, weil das Literal “a” nicht resolviert werden könnte (kann mir jemand erklären was ich hier nicht Verstanden habe)
UP:
{a,b} { a’, c} { c’, d} {a} = {c} {c’, d} - (Was ist hier mit dem “b” passiert?)
hier ist mir auch wieder nicht klar warum das funktioniert, weil:
{a,b} { a’, c} { c’, a’} {a} = {c} {c’} = leer -----------wenn man aber Resolution anwenden würde, würde ja “b” übrig bleiben
Grundsätzlich musst du differenzieren, mit PLE und UP veränderst du die Klauselmenge dahingehend, dass du sie vereinfachst, aber noch das gleiche Ergebnis bekommst.
Mit dem Resolutionsverfahren erzeugst du neue Klauseln, die du dazunimmst. Heißt, wenn du c und ~c resolierst, kommt die leere Menge hinzu, aber c und ~c bleiben weiterhin erhalten. Da aber jetzt die leere Menge ( = FALSE) mit dabei ist, und du die Klauseln untereinander verundest, ist die Formel nicht mehr erfüllbar
[quote=[hedgehogs dilemma = 42]:1426154085]
Ich habe noch Fragen zu UP und PLE.
Hier hätte ich aber folgendes Gegenbeispiel:
{b} {a , b} {c} {c’} = “leer” (nach PLE) - das macht aber keinen Sinn, weil das Literal “a” nicht resolviert werden könnte (kann mir jemand erklären was ich hier nicht Verstanden habe)
[/quote]
Also nach PLE kommt erst mal {C}, {~C} raus - das kannst du dann ganz normal resolieren (?), da kommt dann “leer” raus.
[quote=[hedgehogs dilemma = 42]:1426154085]
UP:
{a,b} { a’, c} { c’, d} {a} = {c} {c’, d} - (Was ist hier mit dem “b” passiert?)
[/quote]
Das ist dem PLE von oben zum Opfer gefallen, da man hinten {a} hat.
[quote=[hedgehogs dilemma = 42]:1426154085]
hier ist mir auch wieder nicht klar warum das funktioniert, weil:
{a,b} { a’, c} { c’, a’} {a} = {c} {c’} = leer -----------wenn man aber Resolution anwenden würde, würde ja “b” übrig bleiben
[/quote]
Das a’ ist durch das UP weggefallen, da, wenn ja a → true, dann muss ~a → false, also bleibt in der zweiten Klausel nur c übrig, in der dritten nur ~c, die wieder resulieren.
Wenn du normal Resolution anwendest, würde man 2. mit 4., 3. mit 4., und dann c mit ~c → Gleiches Ergebnis (Was auch so sein muss - wurde ja bewiesen)
1 „Gefällt mir“
Ich hatte am Anfang einen Denkfehler und zwar hatte ich irgendwie vergessen, dass es ja bei Resolution nur darum geht, dass man irgendwie auf die leere Menge kommt und es dabei egal ist mit welchen Klauseln.
trotzdem, scheint hier noch ein Fehler in dem Tafelanschrieb von unserer Tutorin zu sein.
{a,b} { a’, c} { c’, d} {a} = {c} {c’, d}
das müsste eigentlich
{c} {c’, d} {a} sein, laut Wikipedia (http://en.wikipedia.org/wiki/Unit_propagation)
kann das jemand verifizieren?
Nunja, {a} wird ja als true aufgefasst, weswegen man ja auch die Klausel {a,b} weglassen kann und das a’ in {a’,c} gestrichen wird.
Für die KNF hat die Klausel {a} somit keine Bedeutung mehr, da sie sowieso immer wahr ist.
Also meiner Meinung nach müsste es Stimmen was die Tutorin schrieb.