Notizen SAT, UNSAT, etc. (Update 2)

eintopf
Mausschubser
Mausschubser
Beiträge: 67
Registriert: 25. Aug 2011 17:41

Notizen SAT, UNSAT, etc. (Update 2)

Beitrag von eintopf » 1. Sep 2011 10:27

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.
Dateianhänge
SATUNSATFUCKSAT.pdf
(79.45 KiB) 276-mal heruntergeladen
Zuletzt geändert von eintopf am 1. Sep 2011 19:21, insgesamt 7-mal geändert.

Matthias Senker
Windoof-User
Windoof-User
Beiträge: 41
Registriert: 14. Okt 2010 22:42

Re: Notizen SAT, UNSAT, etc.

Beitrag von Matthias Senker » 1. Sep 2011 11:32

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."
Zuletzt geändert von Matthias Senker am 1. Sep 2011 11:35, insgesamt 1-mal geändert.

fscheepy
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 153
Registriert: 14. Dez 2009 21:17

Re: Notizen SAT, UNSAT, etc.

Beitrag von fscheepy » 1. Sep 2011 11:34

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 :(

eintopf
Mausschubser
Mausschubser
Beiträge: 67
Registriert: 25. Aug 2011 17:41

Re: Notizen SAT, UNSAT, etc.

Beitrag von eintopf » 1. Sep 2011 11:49

Matthias Senker hat geschrieben: Aber meiner Meinung nach müssten FINSAT(FO) und FINUNSAT(FO) Komplemente voneinander sein.
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))
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.")
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: 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."
Done, danke!
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
Folie 112 (letzter Foliensatz, Seite 4)

Ankou
Mausschubser
Mausschubser
Beiträge: 85
Registriert: 15. Mai 2011 18:23

Re: Notizen SAT, UNSAT, etc.

Beitrag von Ankou » 1. Sep 2011 12:08

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))
mMn ist FINUNSAT(FO) die Menge aller Formeln ohne endliches Modell, wie Matthias es auch geschrieben hat, eine genaue Definition hab ich nicht gefunden.
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?

Matthias Senker
Windoof-User
Windoof-User
Beiträge: 41
Registriert: 14. Okt 2010 22:42

Re: Notizen SAT, UNSAT, etc.

Beitrag von Matthias Senker » 1. Sep 2011 12:26

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))
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.
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.
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!
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
Mausschubser
Mausschubser
Beiträge: 67
Registriert: 25. Aug 2011 17:41

Re: Notizen SAT, UNSAT, etc.

Beitrag von eintopf » 1. Sep 2011 12:43

Matthias Senker hat geschrieben:
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))
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.
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.
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!
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.
Ok, denke ich habe es nun verstanden, dazu stell ich gleich ein Update ein.
Man könnte doch sagen, dass FINUNSAT INF0(FO) enthällt oder?

Matthias Senker
Windoof-User
Windoof-User
Beiträge: 41
Registriert: 14. Okt 2010 22:42

Re: Notizen SAT, UNSAT, etc. (Update 2)

Beitrag von Matthias Senker » 1. Sep 2011 13:10

eintopf hat geschrieben:Man könnte doch sagen, dass FINUNSAT INF0(FO) enthällt oder?
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.
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!

eintopf
Mausschubser
Mausschubser
Beiträge: 67
Registriert: 25. Aug 2011 17:41

Re: Notizen SAT, UNSAT, etc. (Update 2)

Beitrag von eintopf » 1. Sep 2011 13:17

Matthias Senker hat geschrieben:
eintopf hat geschrieben:Man könnte doch sagen, dass FINUNSAT INF0(FO) enthällt oder?
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.
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!
Das hört sich gut an.

fscheepy
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 153
Registriert: 14. Dez 2009 21:17

Re: Notizen SAT, UNSAT, etc.

Beitrag von fscheepy » 1. Sep 2011 13:57

eintopf hat geschrieben:
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
Folie 112 (letzter Foliensatz, Seite 4)
Vielleicht habe ich mich ungenau ausgedrückt: Ich frage mich, mit welcher Begründung du diese Teilmengen als unentscheidbar bezeichnet hast.

kain
Mausschubser
Mausschubser
Beiträge: 92
Registriert: 30. Sep 2009 13:49

Re: Notizen SAT, UNSAT, etc. (Update 2)

Beitrag von kain » 1. Sep 2011 18:14

Was noch nützlich wäre:

Zu jeder Menge eine Bsp. - Formel und desen Negat und in welcher Menge diese liegen würde...

eintopf
Mausschubser
Mausschubser
Beiträge: 67
Registriert: 25. Aug 2011 17:41

Re: Notizen SAT, UNSAT, etc. (Update 2)

Beitrag von eintopf » 1. Sep 2011 19:21

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...
dafür hatte ich leider keine Zeit mehr, bzw. die Inklusionen hab ich so weit hingeschrieben wie ich mir sicher bin.

Antworten

Zurück zu „Archiv“