Ich hab da ein Paar Verständnisfragen:
Was ist eine Interpretation der AL? Da gibt es ja die festen Interpretationen für die Junktoren und log. Konstanten.
Ist dann die Interpretation einer Formel die boolesche Auswertung?
Tableau:
Wenn ich eine Verzweigung habe (beta-Regel), muss ich dann eine Formel, die vor der Verzweigung steht ggf. in jedem Zweig einzeln expandieren, wenn ich das benötige oder verstößt das gegen die Striktheit?
PL-Tableau:
Hab bei den Beispielen im Skript nur PL-Formeln ohne Funktionen, also nur mit Prädikaten gesehen. Wo sind denn die Fkt hin? Oder ist das nur ne Teilsprache, für die das Tableau funktioniert?
Woran erkenne ich, dass ein Zweig abgeschlossen ist? Auf Folie 9-5 hätte ich jetzt intuitiv gesagt, dass das schon abgeschlossen ist, aber da steht ja, dass Abschluss noch nicht möglich ist…
Woran erkenne ich denn, dass ich beim Tableau fertig bin, bzw. dass es nicht weiter geht?
Gibt es eine bestimmte Reihenfolge, die klug wäre, um ein PL-Tableau zu erstellen?
Warum ist die Formel (forAll x) P(x) -> P© Taut und (thereIs x) P(x) -> P© falsifizierbar? Versteh das Bsp. im Skript nicht… Für mich impliziert das erste das zweite…
Ich freuen mich über konstruktive Antworten…
Was ist eine Interpretation der AL? Da gibt es ja die festen Interpretationen für die Junktoren und log. Konstanten.
Ist dann die Interpretation einer Formel die boolesche Auswertung?
Richtig. Die Belegung ordnet den atomaren Formeln Wahrheitswerte zu, und die feste Interpretation der Junktoren besagt ja erst, dass w^w=w ist.
Tableau:
Wenn ich eine Verzweigung habe (beta-Regel), muss ich dann eine Formel, die vor der Verzweigung steht ggf. in jedem Zweig einzeln expandieren, wenn ich das benötige oder verstößt das gegen die Striktheit?
Striktheit sagt ja nur, dass innerhalb eines Zweiges eine Formel nur einmal expandiert werd darf; in anderen Zweigen kann sie natürlich auch genutzt werden. Unter Effizienzbetrachtungen ist es natürlich sinnvoll, nach Möglichkeit erst nur Alpha-Regeln und dann Beta-Regeln anzuwenden.
PL-Tableau:
Hab bei den Beispielen im Skript nur PL-Formeln ohne Funktionen, also nur mit Prädikaten gesehen. Wo sind denn die Fkt hin? Oder ist das nur ne Teilsprache, für die das Tableau funktioniert?
Bei der Definiton der PL steht im Anhang: "Ebenso kann man Funktionssymbole weggelassen und ggf. durch Relationssymbole entsprechende Bedingungen ausdrücken." Also ohne Funktionen (und auch ohne Konstanten) ist die PL gleichmächtig, aber umständlicher.
Woran erkenne ich, dass ein Zweig abgeschlossen ist? Auf Folie 9-5 hätte ich jetzt intuitiv gesagt, dass das schon abgeschlossen ist, aber da steht ja, dass Abschluss noch nicht möglich ist…
Verwirrt mich auch gerade. Zu PL-Tableaus gibts hoffentlich nachher mehr, da bin auch grad bei…
Woran erkenne ich, dass ein Zweig abgeschlossen ist? Auf Folie 9-5 hätte ich jetzt intuitiv gesagt, dass das schon abgeschlossen ist, aber da steht ja, dass Abschluss noch nicht möglich ist…
auf 9-4 ist doch gezeigt wie es zum Abschluss kommt,
auf 9-5 nimmt man ne andere Reihenfolge und bekommt den rechten Strang nicht mehr zu
(warum auch immer),
der linke ist geschlossen, der rechte nicht
Woran erkenne ich, dass ein Zweig abgeschlossen ist? Auf Folie 9-5 hätte ich jetzt intuitiv gesagt, dass das schon abgeschlossen ist, aber da steht ja, dass Abschluss noch nicht möglich ist…
auf 9-4 ist doch gezeigt wie es zum Abschluss kommt,
auf 9-5 nimmt man ne andere Reihenfolge und bekommt den rechten Strang nicht mehr zu
(warum auch immer),
der linke ist geschlossen, der rechte nicht
Also heißt das, dass der rechte Strang nicht geschlossen ist, weil ich nicht Q(c,c) und ~Q(d,d) als Abschluss definieren kann und ich für ~(forall x) Q(x,x) wg. delta-Regel neue Terme nehmen muss ?! Kann ich da denn nicht Substituieren, wie in 9-13? Oder ist das was anderes?
Oder kann ich daraus jetzt sehen, dass diese Formel lediglich erfüllbar ist?
wenn ich mich recht erinnere ist so ein Tableaux-Beweis doch ein Beweis für Unerfüllbarkeit bzw. Tautologie?
man sieht ja in 9-4 dass es geht,
bei 9-5 geht es nicht (nicht mehr nach schlechten Anfang) aber ich hab keine Lust/ Zeit nachzulernen wieso,
und wenn da dieses Beispiel so steht, dann bin ich mir ziemlich sicher dass das auch so stimmt ;),
da hilft wohl auch kein Substituieren mehr
man kann auf diesen Wege die Unerfüllbarkeit nicht zeigen,
dass heißt aber auf keinen Fall dass die Formel erfüllbar ist!,
auch nicht dass es unmöglich ist mit einem anderen Tableauxbeweis der gleichen Sorte den Beweis zu führen (9-4 geht ja),
das heißt nur dass es auf diese Weise nicht geklappt hat
Also heißt das, dass der rechte Strang nicht geschlossen ist, weil ich nicht Q(c,c) und ~Q(d,d) als Abschluss definieren kann und ich für ~(forall x) Q(x,x) wg. delta-Regel neue Terme nehmen muss ?!
Richtig.
Kann ich da denn nicht Substituieren, wie in 9-13? Oder ist das was anderes?
Richtig, 9-13 ist ja auch eine Variante des Standardverfahrens und somit genauso vollständig und korrekt. Du kannst ja auch 9-4 zum Abschluss bringen, indem du genau das machst, was im Kommentar steht, und somit in dem noch offenen Zweig ~Q(d,d) und Q(d,d) hättest.
Was mich an passender Stelle daran erinnert, dass es nicht für jeden Tableau-Beweis inPL auch einen strikten Tablea-Beweis gibt.
Oder kann ich daraus jetzt sehen, dass diese Formel lediglich erfüllbar ist?
Da auf 9-4 ihre Unerfüllbarkeit mit Tableau-Beweis geführt wird, kann sie nicht erfüllbar sein. Ein nicht-abgeschlossens Tableau sagt gar nix aus. Das Tableau-Verfahren ist nunmal semi-entscheidbar, nicht entscheidbar (vgl. F3).
Notiz an mich: Häufiger mal die Vorschau benutzen, spart das Editieren…
