Definition von UNSAT und FINUNSAT

patrix
Mausschubser
Mausschubser
Beiträge: 71
Registriert: 16. Nov 2009 17:10

Definition von UNSAT und FINUNSAT

Beitrag von patrix » 26. Aug 2010 00:00

Hallo zusammen,
ich habe eine Frage, bezüglich UNSAT und FINUNSAT (UNSAT ist das Komplement von SAT und FINUNSAT ist das Komplement von FINSAT).
Es gilt ja, dass FINUNSAT\(\subset\)UNSAT. Also darf ja weder UNSAT aber vor allem FINUNSAT nicht rekursiv aufzählbar sein sonst müsste ja auch FINSAT entscheidbar sein was es aber nach dem Satz von Traktenbrot nicht ist?

Danke und viele Grüße Patrick

franzose
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 146
Registriert: 9. Okt 2009 00:08

Re: Definition von UNSAT und FINUNSAT

Beitrag von franzose » 26. Aug 2010 01:54

UNSAT sind die unerfüllbaren Formeln. Diese sind dann über Sequenzenkalkül rekursiv aufzählbar (denn sie sind das Negat von den allgemeingültigen).

daraus folgt aber nicht, dass das Komplement von FINSAT (= alle erfüllbaren in endlichen Modellen, rekursiv aufzählbar) auch aufzählbar ist. Das Komplement müssten alle unerfüllbaren und alle erfüllbaren aber nur in unendlichen Modellen sein.


Genauso ist es mit VAL und FINVAL:

VAL ist rekursiv aufzählbar (Sequenzenkalkül, alle allgemeingültigen).

FINVAL sind alle allgemeingültigen in endlichen Modellen (also alle aus VAL und zusätzlich noch allgemeingültige in nur endlichen Modellen). Das Negat von diesen Formeln sind alle unerfüllbaren und alle erfüllbaren nur in unendlichen Modellen und das ist (siehe oben) nicht aufzählbar, also ist FINVAL nicht aufzählbar.

Das Komplement von FINVAL sind nicht allgemeingültige Formeln in endlichen Modellen (also gibt es wenigstens ein endliches Modell, das die Formel falsch macht). das Negat davon ist erfüllbar in endlichen Modellen. Das ist rekursiv aufzählbar (FINSAT).



Ich hoffe ich habe nicht zu viel dureinander gebracht........
Zuletzt geändert von franzose am 27. Aug 2010 22:17, insgesamt 1-mal geändert.

patrix
Mausschubser
Mausschubser
Beiträge: 71
Registriert: 16. Nov 2009 17:10

Re: Definition von UNSAT und FINUNSAT

Beitrag von patrix » 26. Aug 2010 10:57

Hi vielen Dank für Deine Antwort!
Ich versuche es mal zusammenzufassen:

UNSAT
Beschreibung: alle unerfüllbaren Formlen in unendlichen Formelmengen
Komplement: VAL
Beinhaltet: -
entscheidbar: ja, da UNSAT und Komplement (VAL) rekursiv aufzählbar
Beweis: Sequenzkalkül, Resolution

VAL
Beschreibung: alle allgemeingültigen Formeln in unendlichen Formelmengen
Komplement: UNSAT
Beinhaltet: -
rekursiv aufzählbar: ja
entscheidbar: ja, da VAL und Komplement (UNSAT) rekursiv aufzählbar
Beweis: Sequenzkalkül, Resolution

FINVAL
Beschreibung: alle allgemeingültigen Formeln in endlichen Formelmengen
Komplement: FINUNSAT\(\cup\)INF
Beinhaltet: VAL\(\subset\)FINVAL
rekursiv aufzählbar: ja
entscheidbar: nein, da INF nicht rekursiv aufzählbar
Beweis: Tarski

INF
Beschreibung: alle erfüllbaren Formeln in unendlichen Formelmengen
Komplement: FINVAL\(\cup\)FINSAT\(\cup\)Sätze \(\varphi\) die keine Modelle haben
Beinhaltet:-
rekursiv aufzählbar: nein
entscheidbar: nein
Beweis: Church-Turing

FINSAT
Beschreibung: alle erfüllbaren Formeln in endlichen Formelmengen
Komplement: FINUNSAT\(\cup\)INF
Beinhaltet: -
rekursiv aufzählbar: ja
entscheidbar: nein, da INF nicht rekursiv aufzählbar
Beweis: Traktenbrot

FINUNSAT
Beschreibung: alle unerfüllbaren Formeln in endlichen Formelmengen
Komplement: FINVAL\(\cup\)INF
Beinhaltet: UNSAT\(\subset\)FINUNSAT
rekursiv aufzählbar: ja
entscheidbar: nein, da INF nicht rekursiv aufzählbar
Beweis: ?

SAT
Beschreibung: alle erfüllbaren Formeln in endlichen Formelmengen und unendliche Formlemengen
Komplement: FINUNSAT?
Beinhaltet: FINSAT\(\subset\)INF
rekursiv aufzählbar: nein
entscheidbar: nein
Beweis: Church Turing


Stimmt das soweit?
Verbesserungen sind mehr als willkommen :)

Viele Grüße Patrick

Benutzeravatar
bruse
Kernelcompilierer
Kernelcompilierer
Beiträge: 412
Registriert: 2. Aug 2006 22:42

Re: Definition von UNSAT und FINUNSAT

Beitrag von bruse » 26. Aug 2010 11:47

Hallo Patrick, da ist leider eine ganze Menge falsch. Z.B. ist das Komplement von VAL nicht UNSAT, dafür liegt INF in FINUNSAT, aber FINUNSAT ist nicht das Komplement von FINVAL usw. Schau Dir am besten nochmal die Definitionen in Ruhe an oder geh in eine Sprechstunde.
Un hombre de frente a una ventana
Súper lúcida la mirada
Recorre el paisaje y no,
no es su interior, es luna.

patrix
Mausschubser
Mausschubser
Beiträge: 71
Registriert: 16. Nov 2009 17:10

Re: Definition von UNSAT und FINUNSAT

Beitrag von patrix » 26. Aug 2010 14:32

Das werde ich wohl am besten tun...
Danke und Grüße Patrick

franzose
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 146
Registriert: 9. Okt 2009 00:08

Re: Definition von UNSAT und FINUNSAT

Beitrag von franzose » 26. Aug 2010 19:00

eine kleine Anmerkung noch (es kam mir vor, dass das bei Dir noch nicht so ganz klar ist. Wenn nicht schadet es aber auch nicht, dass es hier steht)

es gibt einen Unterschied zwischen Negat von einer Formel und das Komplement von einer Menge wie SAT, FINVAL etc.

Bsp: für eine allgemeingültige Formel (aus VAL) heisst das ja, dass jedes beliebige Modell die Formel wahr macht. Das Negat dieser Formel ist die Verneinung, also eine Formel, die egal was für ein Modell man nimmt niemals wahr wird (also unerfüllbar --> UNSAT)

das heisst aber nicht, dass UNSAT das Komplement von VAL ist, denn das Komplement von VAL sind einfach alle Formeln, die nicht allgemeingültig sind (d.h. sie können sehr wohl erfüllbar sein und somit nicht in UNSAT, aber es gibt mindestens ein Modell, was die Formel falsch macht)

Antworten

Zurück zu „Archiv“