Resolutionsverfahren < Krypt.+Kod.+Compalg. < Theoretische Inform. < Hochschule < Informatik < Vorhilfe
|
Status: |
(Frage) überfällig | Datum: | 15:47 So 12.11.2006 | Autor: | Phoney |
Aufgabe | Man zeige mit Hilfe des Resolutionsverfahren, dass
$|-((F [mm] \wedge [/mm] G) [mm] \rightarrow [/mm] (H [mm] \rightarrow [/mm] G)) $
Geben Sie dabei die Klauselmenge und jeden Resolventen, den Sie zur Herleitung der leeren Klausel verwenden, an. |
Hallo.
Ich habe da ein Problem mit dem Resolutionsverfahren. Also erst einmal muss ich sagen |- soll das Zeichen für die Tautologie (immer erfüllt) sein. Ich habe es hier im Formeleditor aber nicht gefunden.
Ich forme nun erst einmal sofort um, da ich das Zeichen [mm] \rightarrow [/mm] so gar nicht kenne, ich weiss Aber, dass [mm] A\rightarrow [/mm] B das gleiche ist wie [mm] $\neg [/mm] A [mm] \vee [/mm] B$
Und damit geht es los
$|-((F [mm] \wedge [/mm] G) [mm] \rightarrow [/mm] (H [mm] \rightarrow [/mm] G)) $
$|-((F [mm] \wedge [/mm] G) [mm] \rightarrow (\neg [/mm] H [mm] \vee [/mm] G)) $
[mm] $|-((\neg [/mm] (F [mm] \wedge [/mm] G) [mm] \vee (\neg [/mm] H [mm] \vee [/mm] G))$
[mm] $|-(\neg [/mm] F [mm] \vee \neg [/mm] G) [mm] \vee (\neg [/mm] H [mm] \vee [/mm] G))$
Die Klammern sind ja in diesem Fall sogar egal, also folgt daraus
[mm] $|-(\neg [/mm] F [mm] \vee \neg [/mm] G [mm] \vee \neg [/mm] H [mm] \vee [/mm] G)$
Und jetzt soll ich zwei Striche ziehen und sagen, dass wegen [mm] \neg [/mm] G und (eigentlich ja oder ;) ) G, die Aussage immer wahr ist? Oder was ist zu tun?
Das mit der Klauselmenge habe ich ja jetzt gar nicht gemacht. Was ist da zu tun?
Danke euch.
Gruß
Johann
|
|
|
|
Status: |
(Mitteilung) Reaktion unnötig | Datum: | 16:24 Mi 13.12.2006 | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|