Resolution/Sequenzenkalkül

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Resolution/Sequenzenkalkül

Beitrag von John » 5. Sep 2010 15:50

Eine Aufgabe aus der Klausur vom 1. August 05:
Zu S = {f} (f einstelliges Funktionssymbol) sei
\(\Phi := \{\forall x \neg f x = x, \forall x \neg f f x = x, \forall x \neg f f f x = x, ... \}\)
\(\varphi := \forall x \forall y (\neg x = y \rightarrow \neg f x = f y)\)

Gilt \(\Phi \models \varphi\)? Begründen Sie Ihre Antwort.
Die Folgerung mal paraphrasiert: "Gegeben sei eine Funktion f, die nie eine Zahl bei x-maliger Anwendung auf sich selbst abbildet. Also eine Art Nachfolgerfunktion. Dann folgt daraus, dass diese Funktion nie zwei verschiedene Zahlen auf dieselbe Zahl abbildet."

Irgendwie scheiter ich hier, das Resolutionskalkül oder gar Sequenzenkalkül anzuwenden. Hat jemand eine Idee?

Ich bin jedenfalls zum Ergebnis gekommen, dass die Folgerung nicht stimmt. Dazu hab ich ein Gegenbeispiel genannt, nämlich die Struktur \(R = (\mathbb{R}, f^R)\), wobei \(\mathbb{R}\) die Menge der rellen Zahlen ist, und \(f^R(x) := \lceil x \rceil + 1\). Nun gilt \(\forall x( \neg f^n x = x)\) für alle \(n \in \mathbb{N^+}\), somit ist die Prämisse erfüllt. Die Konklusion stimmt allerdings nicht, denn \(0,9 \neq 1\), aber \(f^R(0,9) = f^R(1)\).

Das Problem ist, für die Lösung hab ich viel zu lange nachgedacht, das ganze muss doch auch algorithmisch mit einem Kalkül widerlegbar sein?
DON'T PANIC

JulM
Mausschubser
Mausschubser
Beiträge: 47
Registriert: 1. Okt 2009 19:25

Re: Resolution/Sequenzenkalkül

Beitrag von JulM » 5. Sep 2010 16:43

Müsste man da nicht einfach nur mit Hilfe des Sequenzkalükls zeigen das \(\Phi \vdash \varphi\) ableitbar ist?
Denn laut Gödelsche Vollständigkeitssatz folgt aus \(\Phi \vdash \varphi \leftrightarrow \Phi \models \varphi\)

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Resolution/Sequenzenkalkül

Beitrag von John » 5. Sep 2010 17:05

Theoretisch hast du Recht, aber zum einen ist die Folgerung (meiner Erkenntnis nach) falsch, und zum anderen ist die Formelmenge \(\Phi\) unendlich, und daher nicht einfach aufschreibbar. Um die Folgerung also zu widerlegen, müsste gezeigt werden, dass \(\neg (\bigwedge \Phi \rightarrow \varphi)\) erfüllbar ist, und dazu kann der Sequenzenkalkül nicht verwendet werden. Und auch die Allgemeingültigkeit dürfte schwierig zu beweisen sein, da du nie die komplette Formelmenge \(\Phi\) auf der linken Seite herleiten kannst.
DON'T PANIC

fetzer
Kernelcompilierer
Kernelcompilierer
Beiträge: 522
Registriert: 1. Okt 2008 17:18

Re: Resolution/Sequenzenkalkül

Beitrag von fetzer » 5. Sep 2010 20:41

\(\Phi \models \varphi\) ist doch dann unerfüllbar, wenn \(\Phi_0 \subseteq \Phi\) existiert, für das \(\Phi_0 \models \varphi\) unerfüllbar ist, oder irre ich mich da? Mittels Resolutionskalkül beweist du nun die Unerfüllbarkeit für mind. 1 Teilmenge.

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Resolution/Sequenzenkalkül

Beitrag von John » 5. Sep 2010 21:01

Nein, so wie ich das verstehe, hast du da was verdreht. Der Kompaktheitssatz sagt aus, dass \(\Phi \models \varphi\) gdw. eine endliche Teilmenge \(\Phi_0 \subseteq \Phi\) existiert, sodass \(\Phi_0 \models \varphi\). Um \(\Phi \not \models \varphi\) zu zeigen, reicht es nicht, eine endliche Teilmenge von \(\Phi\) zu finden, für die das nicht gilt. Es könnte ja immer noch eine "größere" Teilmenge geben, für die die Folgerung doch wahr ist.

Falls die Folgerung war wäre, dann würde es aber tatsächlig reichen, das für eine endliche Teilmenge von \(\Phi\) zu zeigen. Da ich aber denke, dass die Folgerung falsch ist, kann ich das so nicht anwenden.
DON'T PANIC

fetzer
Kernelcompilierer
Kernelcompilierer
Beiträge: 522
Registriert: 1. Okt 2008 17:18

Re: Resolution/Sequenzenkalkül

Beitrag von fetzer » 5. Sep 2010 21:29

John hat geschrieben:Der Kompaktheitssatz sagt aus, dass \(\Phi \models \varphi\) gdw. eine endliche Teilmenge \(\Phi_0 \subseteq \Phi\) existiert, sodass \(\Phi_0 \models \varphi\).
Nicht "eine", sondern "jede" ;) Wenn also für eine Teilmenge Unerfüllbarkeit gilt, dann ist auch \(\Phi \models \varphi\) unerfüllbar.

Der Endlichkeitssatz/Kompaktheitssatz lautet folgendermaßen:
Eine (möglicherweise unendliche) Formelmenge ist genau dann erfüllbar, wenn jede endliche Teilmenge erfüllbar ist.

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Resolution/Sequenzenkalkül

Beitrag von John » 5. Sep 2010 21:55

Ok, da bringen wir jetzt beide was durcheinander.. Ich meine nicht den Kompaktheitssatz, sondern deren Korollar. Du meinst den Kompaktheitssatz, allerdings hilft der direkt nicht, da es nicht um Erfüllbarkeit von \(\Phi\) geht, sondern um die Korrektheit von \(\Phi \models \varphi\). Mit der Korrektur, dass es sich um Korollar 4.2 handelt, sollte meine Aussage stimmen.
DON'T PANIC

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

Re: Resolution/Sequenzenkalkül

Beitrag von franzose » 6. Sep 2010 00:35

@fetzer: ich glaube du hast etwas durcheinandergebracht:

Kompakheitssatz: \(\Phi\) ist erfüllbar gdw JEDE endliche \(\Phi_0 \subseteq \Phi\) erfüllbar ist. Um Erfüllbarkeit von \(\Phi\) zu zeigen, muss man zeigen/begründen/argumentieren, dass ALLE endlichen Teilmengen wahr werden. Um Erfüllbarkeit zu widerlegen genügt es zu zeigen, dass EINE konkrete endliche Teilmenge unerfüllbar ist.

Hier handelt es sich aber um das Korollar: \(\Phi \models \varphi\) gdw EINE endliche \(\Phi_0 \subseteq \Phi\) existiert mit \(\Phi_0 \models \varphi\). Also genügt es hier wirklich EINE konkrete endliche Teilmenge \(\Phi_0\) anzugeben, aus der \(\varphi\) folgt.

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Resolution/Sequenzenkalkül

Beitrag von John » 9. Sep 2010 20:36

Hat vielleicht doch noch jemand hier ne Idee wie man die Folgerung mit Sequenzenkalkül oder Resolutionskalkül oder Kompaktheitssatz beweisen/widerlegen kann? Ich komm nicht drauf..
DON'T PANIC

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

Re: Resolution/Sequenzenkalkül

Beitrag von bruse » 9. Sep 2010 23:55

Naja, Du hast ja gesehen, dass das große Phi das kleine phi nicht impliziert, weil Du ein Modell gefunden hast, in dem Phi gilt, aber phi nicht. Um das maschinell zu zeigen, musst Du beweisen, dass PHI vereinigt nicht phi erfüllbar ist. Was weisst Du über SAT(FO)?
Un hombre de frente a una ventana
Súper lúcida la mirada
Recorre el paisaje y no,
no es su interior, es luna.

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Resolution/Sequenzenkalkül

Beitrag von John » 10. Sep 2010 00:36

SAT(FO) ist unentscheidbar, da hast du Recht, aber vielleicht hab ich auch woanders was übersehen, vielleicht ist auch mein Gegenbeispiel falsch. Mir erschien es unwahrscheinlich, dass man in der Klausur schnell und unter Druck ein solches finden soll. Aber wahrscheinlich lieg ich da falsch..
DON'T PANIC

Antworten

Zurück zu „Archiv“