Beweis zur Resolution < Aussagenlogik < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
| Status: |
(Frage) überfällig  | | Datum: | 17:09 Sa 16.05.2009 | | Autor: | Wimme |
| Aufgabe | Zu Zeigen:
Die Erfüllbarkeit einer Klauselmenge K ändert sich nicht, wenn man aus K alle Klauseln ausschließt, die eine Variable enthalten, welche nur positiv oder nur negativ in K vorkommt. |
AV X komme nur pos./neg. in K vor.
z.z. Interpretation J.
J [mm] \vDash [/mm] K [mm] \Leftrightarrow [/mm] J [mm] \vDash [/mm] K \ [mm] \{C: C \mbox{ enthaelt } X \}
[/mm]
Beweis:
[mm] \Rightarrow [/mm] ist trivial. Wenn man Klauseln entfernt, bleibt die Erfüllbarkeit erhalten.
[mm] \Leftarrow [/mm] Hier habe ich meine Probleme. Wenn X=1 (für nur pos.X) ist, ändert das hinzufügen der Klauseln nix, weil diese ja eh schon erfüllt sind. Was ist aber, wenn X=0 gilt?
Da finde ich kein gutes Argument.
Man könnte aber vielleicht argumentieren:
Wenn man die Resolution auf die Klauselmenge K ausführt, sind die Klauseln mit X unerheblich, denn das X kann nie "eliminiert" werden und damit nicht zur leeren Klausel beitragen.
Das erscheint mir aber kein besonders formaler Beweis zu sein 
Kann mir jemand einen Tipp geben?
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 17:20 Mi 20.05.2009 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
