Resolventen berechnen < Aussagenlogik < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
| Status: |
(Frage) beantwortet  | | Datum: | 14:23 Mi 25.04.2012 | | Autor: | durden88 |
| Aufgabe | Nutzen sie die Resolutionsmethode um zu beweisen, dass die Menge [mm] K_1 [/mm] erfüllbar ist oder nicht.
[mm] K_1=\{\{\neg X,\neg Z\}, \{X,Y\},\{\neg Y\},\{\neg Y,Z,X\}\} [/mm] |
So halli Hallo (wahrscheinlich Tobi gg ;) )
Also das Prinzip ist ja eigendlich ganz einfach. Ich habe dennoch ein paar Fragen dazu:
1. Also ich nehme mir zwei Resolventen und schaue ob da eine positive und ein negative Aussage gleicher Art ist und der Rest wird meine neue Resolvente. Wenn ich irgendwann eine leere Menge erhalte, ist sie unerfüllbar. Die Frage ist, wann ist sie erfüllbar? Irgendwann komme ich wahrscheinlich in eine Endlosschleife. Ab wann sehe ich das bzw. wie macht sich das bemerkbar?
2. In dieser Aufgabe habe ich nun in der ersten runde alle neuen Resolventen ausgerechnet. Diese Resolventen berechne ich nun zum ersten wieder miteinander und zum zweiten auch mit den Ausgangsresolventen der [mm] K_1?
[/mm]
Bei dieser Aufgabe habe ich dann am Ende stehen (das ist 1,5 Jahre her als ich das aufgeschrieben habe, ich weiß nichtmehr warum ich das gemacht habe):
[mm] ...Res^\infty(K_1)= [/mm] (das muss man herausfinden) [mm] Res^2(K_1)
[/mm]
Was bedeutet das, also wenn die Resolution ins Unendliche geht dann ist es erfüllbar? [mm] Res^2 [/mm] habe ich ja dann im zweiten Schritt gebildet, aber wie sehe ich das es gegen das Unendliche geht?
Liebe Grüße und Danke!
|
|
| |
|
| Status: |
(Antwort) fertig  | | Datum: | 19:34 Mi 25.04.2012 | | Autor: | tobit09 |
Hallo durden,
> So halli Hallo (wahrscheinlich Tobi gg ;) )
Da muss ich wohl reagieren...  Habe zwar bis eben noch nie etwas von Resolventen gehört, aber ich habe ja dein Skript.
> Also das Prinzip ist ja eigendlich ganz einfach. Ich habe
> dennoch ein paar Fragen dazu:
>
> 1. Also ich nehme mir zwei Resolventen Klauseln und schaue ob da
> eine positive und ein negative Aussage gleicher Art ist
> und der Rest wird meine neue Resolvente. Wenn ich
> irgendwann eine leere Menge erhalte, ist sie unerfüllbar.
> Die Frage ist, wann ist sie erfüllbar?
Genau dann, wenn du bei dieser Vorgehensweise nicht die leere Menge erhältst.
> Irgendwann komme
> ich wahrscheinlich in eine Endlosschleife. Ab wann sehe ich
> das bzw. wie macht sich das bemerkbar?
Wenn du in einem Schritt keine neuen Resolventen kriegst, kannst du so viele Schritte machen wie du willst: Du wirst nie weitere Resolventen finden.
> 2. In dieser Aufgabe habe ich nun in der ersten runde alle
> neuen Resolventen ausgerechnet. Diese Resolventen berechne
> ich nun zum ersten wieder miteinander und zum zweiten auch
> mit den Ausgangsresolventenklauseln der [mm]K_1?[/mm]
Ja.
> Bei dieser Aufgabe habe ich dann am Ende stehen (das ist
> 1,5 Jahre her als ich das aufgeschrieben habe, ich weiß
> nichtmehr warum ich das gemacht habe):
>
> [mm]...Res^\infty(K_1)=[/mm] (das muss man herausfinden) [mm]Res^2(K_1)[/mm]
>
> Was bedeutet das, also wenn die Resolution ins Unendliche
> geht dann ist es erfüllbar? [mm]Res^2[/mm] habe ich ja dann im
> zweiten Schritt gebildet, aber wie sehe ich das es gegen
> das Unendliche geht?
Egal, ob erfüllbar oder nicht: Nach endlich vielen Schritten kommen keine neuen Resolventen hinzu. Hast du dann keine Klausel dabei, die die leere Menge ist, so war die Ausgangsformel erfüllbar. Anderenfalls ist sie nicht erfüllbar. In diesem Fall kannst du natürlich schon nach dem Schritt, in dem du die leere Menge erhältst, die Suche nach weiteren Resolventen einstellen.
Viele Grüße
Tobias
|
|
|
| |
|
| Status: |
(Frage) beantwortet | | Datum: | 14:21 Mo 30.04.2012 | | Autor: | durden88 |
So jetzt hab ich nochmal eine Frage dazu :)
Also ich habe jetzt die ersten Klausueln von [mm] K_1 [/mm] mit den Klauseln von [mm] K_1^2 [/mm] verknüpft. Und da bei manchen Verknüpfungen die gleichen Ergebnisse raus. Was heißt das nun für mich? Muss ich dann mit denen weiter rechnen wo nicht die gleichen Sachen rauskommen?
|
|
|
| |
|
| Status: |
(Antwort) fertig | | Datum: | 14:43 Mo 30.04.2012 | | Autor: | tobit09 |
> Also ich habe jetzt die ersten Klausueln von [mm]K_1[/mm] mit den
> Klauseln von [mm]K_1^2[/mm] verknüpft.
Was ist [mm] $K_1^2$? [/mm] Meinst du [mm] $Res^2(K_1)$?
[/mm]
> Und da bei manchen
> Verknüpfungen die gleichen Ergebnisse raus. Was heißt das
> nun für mich? Muss ich dann mit denen weiter rechnen wo
> nicht die gleichen Sachen rauskommen?
Die Mengen [mm] $Res^n(K_1)$, [/mm] die du nacheinander ermittelst, sind wirklich Mengen, d.h. sie enthalten jedes Element nur einmal. Du brauchst also doppelte Vorkommen nicht doppelt aufzuführen.
|
|
|
| |
|
| Status: |
(Frage) beantwortet | | Datum: | 15:25 Mo 30.04.2012 | | Autor: | durden88 |
Also muss ich wirklich soweit weiter rechnen, bis ich keine neuen mehr bekomme? Also nicht warten bis sich eins wiederholt hat?
|
|
|
| |
|
| Status: |
(Antwort) fertig | | Datum: | 17:15 Mo 30.04.2012 | | Autor: | tobit09 |
> Also muss ich wirklich soweit weiter rechnen, bis ich keine
> neuen mehr bekomme? Also nicht warten bis sich eins
> wiederholt hat?
Leider ja. Es sei denn, du erhältst schon vorher die leere Menge.
|
|
|
| |
|
Also ich habe jetzt 3 Blätter vollgeschrieben. bei [mm] Res^3....und [/mm] das schöne war bei allen Kombies kam das gleiche raus wie aus Res oder [mm] Res^2 [/mm] bis auf 5 Klauseln...gibt es im Internet vielleicht sowas wie ein Resolventenplotter oder sowas, womit ich mein Ergebnis überprüfen kann?
|
|
|
| |
|
| Status: |
(Antwort) fertig | | Datum: | 09:32 Di 01.05.2012 | | Autor: | tobit09 |
> Also ich habe jetzt 3 Blätter vollgeschrieben. bei
> [mm]Res^3....und[/mm] das schöne war bei allen Kombies kam das
> gleiche raus wie aus Res oder [mm]Res^2[/mm] bis auf 5
> Klauseln...
Tatsächlich erscheint mir die Resolventenmethode sehr aufwändig von Hand durchzuführen. Ihr Vorteil liegt vermutlich bei einer großen Zahl vorkommender Variablen, wenn die Wahrheitstafel sehr aufwändig wäre. Bei Aufgaben der Größenordnung, dass sie von Hand lösbar sind, dürfte ein Untersuchen der Wahrheitstafel vermutlich schneller gehen und weniger fehleranfällig sein. Wenn aber explizit nach Resolventenmethode gefragt ist, musst du wohl in den sauren Apfel beißen...
> gibt es im Internet vielleicht sowas wie ein
> Resolventenplotter oder sowas, womit ich mein Ergebnis
> überprüfen kann?
Keine Ahnung. Daher lasse ich die Frage auf nur "teilweise beantwortet".
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 13:01 Di 01.05.2012 | | Autor: | durden88 |
Ja also es klappt, super aufwändig aber am Ende kommen die Wiederholten Klauseln aus [mm] Res^2 [/mm] und [mm] Res^1 [/mm] raus und somit ist das Ding erfüllbar.
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig | | Datum: | 18:20 Mi 02.05.2012 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
