Resolution < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
| Status: |
(Frage) beantwortet  | | Datum: | 12:58 So 14.05.2006 | | Autor: | dump_0 |
Hallo Gemeinde!
Ich habe ein kleines Problem mit folgender Aufgabe:
F sei eine aus mindestens zwei Konjunktionen bestehende Formel in DNF und es seien
[tex]K_1 = (A \wedge L_{1,1} \wedge L_{1,2} \wedge \ldots \wedge L_{1,r}[/tex]
und
[tex]K_2 = (\neg A \wedge L_{2,1} \wedge L_{2,2} \wedge \ldots \wedge L_{2,s}[/tex]
zwei der Konjunktionen von F, woberi A eine atomanre Formel, r und s zwei positive natürliche Zahlen und [mm] L_{i,j} [/mm] Literale sind.
Dann ist
[tex]F' = F \vee (L_{1,1} \wedge L_{1,2} \wedge \ldots \wedge L_{1,r} \wedge L_{2,1} \wedge L_{2,2} \wedge \ldots \wedge L_{2,s}[/tex]
semantisch äquivalent zu F.
a) Beweisen Sie die Korrektheit dieser Aussage
b) Welches "Resolutionsverfahren" ergibt sicha us der Ausssage? Wozu dient es (d.h. was lässt sich damit über eine Formel in DNF herausfinden?)
Wie soll ich denn am besten hier vorgehen? Ich kann ja nicht einfach die Resolutonsmethode anwenden, da diese ja nur für Formeln in KNF gilt. Muss ich hier also zuerst die Formel in eine allg. KNF-Formel umwandeln und dann die Resolutionsmehtode anwenden und anschließend wieder in DNF umwandeln oder geht es auch anders?
Ich würde mich über eure Hilfe freuen :)
Grüße
[mm] dump_0
[/mm]
|
|
| |
|
Hallo und guten Morgen,
>
> [tex]K_1 = (A \wedge L_{1,1} \wedge L_{1,2} \wedge \ldots \wedge L_{1,r}[/tex]
>
> und
>
> [tex]K_2 = (\neg A \wedge L_{2,1} \wedge L_{2,2} \wedge \ldots \wedge L_{2,s}[/tex]
>
> zwei der Konjunktionen von F, woberi A eine atomanre
> Formel, r und s zwei positive natürliche Zahlen und [mm]L_{i,j}[/mm]
> Literale sind.
>
> Dann ist
>
> [tex]F' = F \vee (L_{1,1} \wedge L_{1,2} \wedge \ldots \wedge L_{1,r} \wedge L_{2,1} \wedge L_{2,2} \wedge \ldots \wedge L_{2,s}[/tex]
>
> semantisch äquivalent zu F.
>
Semantisch heisst wohl: Die Modelle sind dieselben, d.h.
[mm] {\mathcal A} \models [/mm] F genau dann, wenn
[mm] {\mathcal A} \models [/mm] F'
Das ergibt sich doch direkt durch Anwenden der Definition der Modellbeziehung und miitels Prädikatenlogik (wenn die L's alle wahr sind,
so wird genau eine der beiden Klauseln wahr sein, also folgt [mm] {\mathcal A}\models [/mm] K).
Ganz genau:
[mm] {\mathcal A} \models [/mm] F gdw
[mm] {\mathcal A} \models K_1 [/mm] oder [mm] {\mathcal A} \models K_2 [/mm] oder [mm] {\mathcal A} \models [/mm] F gdw
[mm] {\mathcal A} \models [/mm] F oder [mm] {\mathcal A} \models F\vee \underbrace{((K_1\wedge K_2)\vee (K_1\wedge \neg K_2)\vee (\neg K_1\wedge K_2))}_{(star)}
[/mm]
und den Teil [mm] (\star) [/mm] kann man dann weiter umformen.
Gruss,
Mathias
> a) Beweisen Sie die Korrektheit dieser Aussage
> b) Welches "Resolutionsverfahren" ergibt sicha us der
> Ausssage? Wozu dient es (d.h. was lässt sich damit über
> eine Formel in DNF herausfinden?)
>
>
> Wie soll ich denn am besten hier vorgehen? Ich kann ja
> nicht einfach die Resolutonsmethode anwenden, da diese ja
> nur für Formeln in KNF gilt. Muss ich hier also zuerst die
> Formel in eine allg. KNF-Formel umwandeln und dann die
> Resolutionsmehtode anwenden und anschließend wieder in DNF
> umwandeln oder geht es auch anders?
>
>
> Ich würde mich über eure Hilfe freuen :)
>
>
> Grüße
> [mm]dump_0[/mm]
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 19:23 Di 16.05.2006 | | Autor: | dump_0 |
Vielen Dank für deine Antwort!
An die Modelle hatte ich garnicht mehr gedacht :-/
Aber ich hätte trozdem noch ne Frage, und zwar, wenn ich wie du geschirben hast
[tex] {\mathcal A} \models F\vee \underbrace{((K_1\wedge K_2)\vee (K_1\wedge \neg K_2)\vee (\neg K_1\wedge K_2))}_{(star)}[/tex]
schreibe, dann bleibt am Ende
[tex]F \vee (K_1 \wedge K_2)[/tex]
da fliegt dann das A bzw. [mm] \neg [/mm] A raus und es steht dann F' da.
In der Überschrift stand etwas von Resolution für formeln in DNF, aber ich habe hier doch eig. keinerlei resolution angewendet oder geht es auch noch anders über eben diese Methode?
Grüße
[mm] dump_0
[/mm]
|
|
|
|
