Notizen SAT, UNSAT, etc. (Update 2)
Notizen SAT, UNSAT, etc. (Update 2)
Hallo,
da letztes Jahr eine wie ich finde ziemlich miese Aufgabe zu SAT, UNSAT, etc. kam (Diagramm in dem man die Inklusionen etc. einzeichnen musste), habe ich angefangen mir aufzuschreiben, was die Mengen bedeuten und was deren Komplemente und Inklusionen etc. sind.
Bin noch nicht fertig, aber wäre schön wenn ihr daran mitwirken könntet, werde es dann immer aktualisieren.
Viele Grüße!
EDIT:
19:21 - Datei aktuallisiert, Boolesche Algebra Regeln eingefügt, Distributivgesetz etc.
da letztes Jahr eine wie ich finde ziemlich miese Aufgabe zu SAT, UNSAT, etc. kam (Diagramm in dem man die Inklusionen etc. einzeichnen musste), habe ich angefangen mir aufzuschreiben, was die Mengen bedeuten und was deren Komplemente und Inklusionen etc. sind.
Bin noch nicht fertig, aber wäre schön wenn ihr daran mitwirken könntet, werde es dann immer aktualisieren.
Viele Grüße!
EDIT:
19:21 - Datei aktuallisiert, Boolesche Algebra Regeln eingefügt, Distributivgesetz etc.
- Dateianhänge
-
- SATUNSATFUCKSAT.pdf
- (79.45 KiB) 300-mal heruntergeladen
Zuletzt geändert von eintopf am 1. Sep 2011 19:21, insgesamt 7-mal geändert.
-
- Windoof-User
- Beiträge: 41
- Registriert: 14. Okt 2010 22:42
Re: Notizen SAT, UNSAT, etc.
Hi,
im Prinzip finde ich die Liste praktisch. Gute Idee.
Aber meiner Meinung nach müssten FINSAT(FO) und FINUNSAT(FO) Komplemente voneinander sein. Demzufolge dürfte FINUNSAT(FO) dann auch nicht aufzählbar sein, weil ja FINSAT(FO) schon aufzählbar ist. Und wenn FINUNSAT(FO) nicht aufzählbar ist, dann ist auch FINVAL(FO) nicht aufzählbar. (steht auch im Skript: Seite 37 Über Satz 7.3 (Traktenbrot): "Die Menge der in endlichen Strukturen allgemeingültigen FO-Sätze ist nicht rekursiv aufzählbar.")
Und ich würde die Beschreibung von FINUNSAT(FO) ändern zu:
"Die Menge aller Formeln in FO, die in endlichen Strukturen unerfüllbar sind." oder aber "Die Menge aller Formeln in FO, die kein endliches Modell haben."
Wenn eine Formel nämlich ein Modell hat, ist sie auch erfüllbar! Die bisherige Beschreibung "Alle unerfüllbaren Formeln in FO mit endlichem Modell" ist also ein Widerspruch!
Und auch bei FINVAL(FO) würde ich schreiben:
"Die Menge aller Formeln in FO, die in endlichen Strukturen allgemeingültig sind."
im Prinzip finde ich die Liste praktisch. Gute Idee.
Aber meiner Meinung nach müssten FINSAT(FO) und FINUNSAT(FO) Komplemente voneinander sein. Demzufolge dürfte FINUNSAT(FO) dann auch nicht aufzählbar sein, weil ja FINSAT(FO) schon aufzählbar ist. Und wenn FINUNSAT(FO) nicht aufzählbar ist, dann ist auch FINVAL(FO) nicht aufzählbar. (steht auch im Skript: Seite 37 Über Satz 7.3 (Traktenbrot): "Die Menge der in endlichen Strukturen allgemeingültigen FO-Sätze ist nicht rekursiv aufzählbar.")
Und ich würde die Beschreibung von FINUNSAT(FO) ändern zu:
"Die Menge aller Formeln in FO, die in endlichen Strukturen unerfüllbar sind." oder aber "Die Menge aller Formeln in FO, die kein endliches Modell haben."
Wenn eine Formel nämlich ein Modell hat, ist sie auch erfüllbar! Die bisherige Beschreibung "Alle unerfüllbaren Formeln in FO mit endlichem Modell" ist also ein Widerspruch!
Und auch bei FINVAL(FO) würde ich schreiben:
"Die Menge aller Formeln in FO, die in endlichen Strukturen allgemeingültig sind."
Zuletzt geändert von Matthias Senker am 1. Sep 2011 11:35, insgesamt 1-mal geändert.
Re: Notizen SAT, UNSAT, etc.
Wie kommst du denn auf deine Aussagen über INF0, INF1 und INF2? Und was ist mit INFVAL(FO) - alle Formeln, die im Unendlichen allgemeingültig sind? Dazu habe ich bisher noch nirgends etwas gefunden 

Re: Notizen SAT, UNSAT, etc.
Das ist die zunächst "intuitive" Überlegung, aber ich habe mir folgendes überlegt:Matthias Senker hat geschrieben: Aber meiner Meinung nach müssten FINSAT(FO) und FINUNSAT(FO) Komplemente voneinander sein.
Das Komplement von FINSAT(FO) enthält FINUNSAT, aber auch viel mehr, es enthält z.B. auch alle Formeln die in unendlichen Modellen erfüllbar sind etc. (allein schon weil FINSAT(FO) eine Teilmenge von SAT(FO))
Bin mir grad nicht ganz sicher mit FINUNSAT, aber glaube du hast Recht. FINVAL ist auf keinen Fall rek. aufzählbar, da geb ich dir absolut Recht!Matthias Senker hat geschrieben: Demzufolge dürfte FINUNSAT(FO) dann auch nicht aufzählbar sein, weil ja FINSAT(FO) schon aufzählbar ist.
Und wenn FINUNSAT(FO) nicht aufzählbar ist, dann ist auch FINVAL(FO) nicht aufzählbar. (steht auch im Skript: Seite 37 Über Satz 7.3 (Traktenbrot): "Die Menge der in endlichen Strukturen allgemeingültigen FO-Sätze ist nicht rekursiv aufzählbar.")
Done, danke!Matthias Senker hat geschrieben: Und ich würde die Beschreibung von FINUNSAT(FO) ändern zu:
"Die Menge aller Formeln in FO, die in endlichen Strukturen unerfüllbar sind." oder aber "Die Menge aller Formeln in FO, die kein endliches Modell haben."
Wenn eine Formel nämlich ein Modell hat, ist sie auch erfüllbar! Die bisherige Beschreibung "Alle unerfüllbaren Formeln in FO mit endlichem Modell" ist also ein Widerspruch!
Und auch bei FINVAL(FO) würde ich schreiben:
"Die Menge aller Formeln in FO, die in endlichen Strukturen allgemeingültig sind."
Folie 112 (letzter Foliensatz, Seite 4)fscheepy hat geschrieben: Wie kommst du denn auf deine Aussagen über INF0, INF1 und INF2? Und was ist mit INFVAL(FO) - alle Formeln, die im Unendlichen allgemeingültig sind? Dazu habe ich bisher noch nirgends etwas gefunden
Re: Notizen SAT, UNSAT, etc.
mMn ist FINUNSAT(FO) die Menge aller Formeln ohne endliches Modell, wie Matthias es auch geschrieben hat, eine genaue Definition hab ich nicht gefunden.Das ist die zunächst "intuitive" Überlegung, aber ich habe mir folgendes überlegt:
Das Komplement von FINSAT(FO) enthält FINUNSAT, aber auch viel mehr, es enthält z.B. auch alle Formeln die in unendlichen Modellen erfüllbar sind etc. (allein schon weil FINSAT(FO) eine Teilmenge von SAT(FO))
Die Menge aller Formeln ohne endlichem Modell ist natürlich das Komplement zur Menge aller Formeln mit einem endlichen Modell, ich wüsste nicht wieso die Formeln, die nur im unendlichen erfüllbar sind nicht in FINUNSAT sein sollten?
-
- Windoof-User
- Beiträge: 41
- Registriert: 14. Okt 2010 22:42
Re: Notizen SAT, UNSAT, etc.
Mir scheint, du hast FINSAT nicht ganz verstanden. Wenn eine Formel in FINSAT ist, dann hat sie ein endliches Modell, aber das heißt NICHT, dass sie keine unendlichen Modelle besitzen darf. Ebenso darf eine Formel in FINUNSAT sehr wohl unendliche Modelle besitzen, nur halt keine endlichen.eintopf hat geschrieben:Das Komplement von FINSAT(FO) enthält FINUNSAT, aber auch viel mehr, es enthält z.B. auch alle Formeln die in unendlichen Modellen erfüllbar sind etc. (allein schon weil FINSAT(FO) eine Teilmenge von SAT(FO))
Daher kann eine Formel, wenn sie ein unendliches Modell besitzt, trotzdem in FINUNSAT sein! Daher bin ich mir eigentlich ziemlich sicher, dass FINSAT und FINUNSAT Komplemente voneinander sind (Eine 3. Meinung wäre vielleicht ganz hilfreich.) EDIT: Danke an Ankou für seine Meinung.
Wenn FINUNSAT rekursiv aufzählbar wäre, dann könnte man auch FINVAL aufzählen, indem man eine Formel, für die man wissen möchte, ob sie in FINVAL ist, einfach negiert und dann das Aufzählverfahren für FINUNSAT anwendet, denn eine Formel ist in endlichen Strukturen allgemeingültig, gdw. wenn ihre Negation in endlichen Strukturen unerfüllbar ist.eintopf hat geschrieben:Bin mir grad nicht ganz sicher mit FINUNSAT, aber glaube du hast Recht. FINVAL ist auf keinen Fall rek. aufzählbar, da geb ich dir absolut Recht!
Re: Notizen SAT, UNSAT, etc.
Ok, denke ich habe es nun verstanden, dazu stell ich gleich ein Update ein.Matthias Senker hat geschrieben:Mir scheint, du hast FINSAT nicht ganz verstanden. Wenn eine Formel in FINSAT ist, dann hat sie ein endliches Modell, aber das heißt NICHT, dass sie keine unendlichen Modelle besitzen darf. Ebenso darf eine Formel in FINUNSAT sehr wohl unendliche Modelle besitzen, nur halt keine endlichen.eintopf hat geschrieben:Das Komplement von FINSAT(FO) enthält FINUNSAT, aber auch viel mehr, es enthält z.B. auch alle Formeln die in unendlichen Modellen erfüllbar sind etc. (allein schon weil FINSAT(FO) eine Teilmenge von SAT(FO))
Daher kann eine Formel, wenn sie ein unendliches Modell besitzt, trotzdem in FINUNSAT sein! Daher bin ich mir eigentlich ziemlich sicher, dass FINSAT und FINUNSAT Komplemente voneinander sind (Eine 3. Meinung wäre vielleicht ganz hilfreich.) EDIT: Danke an Ankou für seine Meinung.
Wenn FINUNSAT rekursiv aufzählbar wäre, dann könnte man auch FINVAL aufzählen, indem man eine Formel, für die man wissen möchte, ob sie in FINVAL ist, einfach negiert und dann das Aufzählverfahren für FINUNSAT anwendet, denn eine Formel ist in endlichen Strukturen allgemeingültig, gdw. wenn ihre Negation in endlichen Strukturen unerfüllbar ist.eintopf hat geschrieben:Bin mir grad nicht ganz sicher mit FINUNSAT, aber glaube du hast Recht. FINVAL ist auf keinen Fall rek. aufzählbar, da geb ich dir absolut Recht!
Man könnte doch sagen, dass FINUNSAT INF0(FO) enthällt oder?
-
- Windoof-User
- Beiträge: 41
- Registriert: 14. Okt 2010 22:42
Re: Notizen SAT, UNSAT, etc. (Update 2)
Nein, denn INF0 enthält zwar alle Formeln, die unendliche Modelle besitzen, verbietet den Formeln aber nicht, ebenso auch endliche Modelle zu besitzen. Und eine Formel mit endlichen Modellen ist ja nicht in FINUNSAT.eintopf hat geschrieben:Man könnte doch sagen, dass FINUNSAT INF0(FO) enthällt oder?
Aber wich würde sagen, dass FINUNSAT INF1 enthält. Denn jede Formel in INF1 ist nur in unendlichen Strukturen erfüllbar, besitzt also kein endliches Modell und ist daher in FINUNSAT.
Ich würde sogar sagen (korrigiert mich, wenn ich mich irre), dass FINUNSAT die Vereinigung von UNSAT und INF1 ist!
Re: Notizen SAT, UNSAT, etc. (Update 2)
Das hört sich gut an.Matthias Senker hat geschrieben:Nein, denn INF0 enthält zwar alle Formeln, die unendliche Modelle besitzen, verbietet den Formeln aber nicht, ebenso auch endliche Modelle zu besitzen. Und eine Formel mit endlichen Modellen ist ja nicht in FINUNSAT.eintopf hat geschrieben:Man könnte doch sagen, dass FINUNSAT INF0(FO) enthällt oder?
Aber wich würde sagen, dass FINUNSAT INF1 enthält. Denn jede Formel in INF1 ist nur in unendlichen Strukturen erfüllbar, besitzt also kein endliches Modell und ist daher in FINUNSAT.
Ich würde sogar sagen (korrigiert mich, wenn ich mich irre), dass FINUNSAT die Vereinigung von UNSAT und INF1 ist!
Re: Notizen SAT, UNSAT, etc.
Vielleicht habe ich mich ungenau ausgedrückt: Ich frage mich, mit welcher Begründung du diese Teilmengen als unentscheidbar bezeichnet hast.eintopf hat geschrieben:Folie 112 (letzter Foliensatz, Seite 4)fscheepy hat geschrieben: Wie kommst du denn auf deine Aussagen über INF0, INF1 und INF2? Und was ist mit INFVAL(FO) - alle Formeln, die im Unendlichen allgemeingültig sind? Dazu habe ich bisher noch nirgends etwas gefunden
Re: Notizen SAT, UNSAT, etc. (Update 2)
Was noch nützlich wäre:
Zu jeder Menge eine Bsp. - Formel und desen Negat und in welcher Menge diese liegen würde...
Zu jeder Menge eine Bsp. - Formel und desen Negat und in welcher Menge diese liegen würde...
Re: Notizen SAT, UNSAT, etc. (Update 2)
dafür hatte ich leider keine Zeit mehr, bzw. die Inklusionen hab ich so weit hingeschrieben wie ich mir sicher bin.kain hat geschrieben:Was noch nützlich wäre:
Zu jeder Menge eine Bsp. - Formel und desen Negat und in welcher Menge diese liegen würde...