+- FB18.de - Das Informatikforum ( /mybb )
+-- Forum: Diplom Informatik ( /forumdisplay.php?fid=114 )
+--- Forum: Unterbereich Grundstudium ( /forumdisplay.php?fid=123 )
+---- Forum: Formale Informatik ( /forumdisplay.php?fid=16 )
+---- Thema: F1: BPF und Skolemform ( /showthread.php?tid=7364 )
F1: BPF und Skolemform - MalagaNt - 08.07.2004 18:42
Ich hab mal ne Frage...
Müssen die Implikationen und Biimplikationen in der BPF eleminiert werden oder nicht? In den Lösungen aus dem WS02/03 wurde dies getan, bei der Skolemform, die ja eine BPF voraussetzt, wiederum nicht ?!
Re: F1: BPF und Skolemform - Anonymer User - 08.07.2004 22:25
BPF = bereinigte Pränexform. (Vgl. hierzu Folie 10[ 8].)
Dort ist nicht davon die rede, dass man Implikation oder Biimplikationen auflösen müsste und auch bei der Skolemisierung wird dies nicht verlangt.
Vergleicht man aber Folie 10[ 24], so kann man in einem weiteren Schritt eine Klauselnormalform herstellen, bei der die Matrix (der Formel in Skolemform) noch in KNF (= Konjunktive Normalform) umgewandelt wird. Hier wiederrum würde man Implikationen und Biimplikationen eleminieren.
Evtl. ist dies (zusätzlich?) bei der Aufgabe im WS02/03 gemacht worden. Auf welche Aufgabe genau beziehst du dich?
Cheers.
[nun siehts wieder lesbar aus ;) - Slater]
Re: F1: BPF und Skolemform - Anonymer User - 08.07.2004 22:27
Pardon. In obigem Text sollten keine Smilies stehen. Ich wollte auf die Folien verweisen:
Gemeint ist zuerste Folie 10-8.
Beim zweiten ist Folie 10-24 gemeint.
Cheers.
Re: F1: BPF und Skolemform - Azure - 08.07.2004 22:33
So - und dann schreibe ich jetzt auch wieder als angemeldeter User. Zum einen hab' ich im Proseminar gelernt, dass das zur Netiquette gehört und zum zweiten kann ich meine Texte dann auch wieder korrigieren
Cheers,
Frank
P.S. Und ausserdem ist mein Lieblingsavatar wieder da
Re: F1: BPF und Skolemform - a nonymous user - 09.07.2004 00:22
Zitat:
Gemeint ist zuerste Folie 10-8.
Beim zweiten ist Folie 10-24 gemeint.
Beim zweiten ist Folie 10-24 gemeint.
*lol* ist mir letztens auch passiert... die Folienangaben mag er nich so...
Re: F1: BPF und Skolemform - MalagaNt - 09.07.2004 15:31
Blatt 13, Aufgaben 1 + 2.
Formel G besteht nur aus Implikationen, die bei der Umwandlung in BPF eleminiert werden, was natürlich exorbitanter Aufwand ist.
Edit:
http://www.malagant.net/tmp/Blatt13.pdf
http://www.malagant.net/tmp/Loesung13.pdf
Re: F1: BPF und Skolemform - Azure - 09.07.2004 17:10
Zitat:
was natürlich exorbitanter Aufwand ist.
Das ist ironisch gemeint, gell?
Aber um nochmal die Frage zu beantworten: Das ist nicht nötig, wenn es um BPF geht (nach der Definition von BPF im Skript). - Evtl. findet der ein oder andere es nur praktischer erst diese Umwandlung vorzunehmen, um bei den Quantoren und der Implikation nicht durcheinander zu geraten.
Cheers,
Frank
Re: F1: BPF und Skolemform - Anonymer User - 12.07.2004 14:53
Und noch einen.
Können in BPF und dememtsprechend in der Skolemvariante Konstanten vorhanden sein.
Ich habe nichts gegenteiliges gelesen, denke ich.
Re: F1: BPF und Skolemform - Azure - 12.07.2004 23:25
Klar. In der Skolemisierung können ja sogar (Skolem-)Konstanten eingeführt werden! (Vgl. 10-{20})
Cheers,
Frank
Re: F1: BPF und Skolemform - pRoMoE - 16.07.2004 15:28
Ich wäre mir da nicht so sicher.
bereinigt bedeutet, dass alle freien variablen durch existenzquantor gebunden werden müssen.
In einer Musterlösung (ich glaueb die erste, die sich mit Prädikatenlogik beschäftigt) steht, dass Konstanten und freie Variablen nichtso einfach (gar nicht?) unterschieden werden können.
Die skolemkonstanten am Ende werden ja auch nur durch die skolemisierung erstellt. DA zur skolemisierung aber eine BPF nötig ist dürfte die (bereinigte)PF auch keine Konstanten mehr enthalten. Kann aber sein, dass jetzt n Denkfehler dabei ist ^^
Re: F1: BPF und Skolemform - Azure - 16.07.2004 18:13
Die Unterscheidung freie Variable/Konstante ist im Prinzip bereits durch die Syntax gegeben! Siehe Folie 9{7} und 9{8}.
Vgl. auch das Beispiel im Schöning - nur um ihn nochmals zu erwähnen
- auf S.67. Hier wird auch eine Formel in (bereinigte) Pränexform, dann in Skolemform (mit Einführung von Skolemkonstanten) und in Klauselnormalform umgeformt.
Hoff' es hilft
Cheers,
Frank
Re: F1: BPF und Skolemform - pRoMoE - 16.07.2004 20:13
Auaua
Jo hab Mist erzählt, bin im Skript in der Zeile verrutscht T_T
Das Binden der freien Variablen ist für die geschlossene Form notwendig
Und die Unterscheidung ist in der Syntax gegeben, in der Musterlösung stand das mit der Einschränkung, dass die Def nicht bekannt seien.
2x Mist in einem post erzählt :/
Im Schöning sind Umformungen in BPF aber ich hab auf Anhieb keine gesehen, bei der in der Grundform Konstanten vorkommen
Auf Seite 62 ist jedoch eine Formel, die in Skolemform umgewandelt werden soll, in welcher eine Konstante vorkommt.
Kann man wohl draus schliessen dass Konstanten anders als freie Variablen nicht gebunden werden müssen (hoffentlich is das jetzt wenigstens richtig)
Re: F1: BPF und Skolemform - Azure - 16.07.2004 22:25
Auf S.67 wird ja eine Formel in Klauselnormalform umgeformt. Dort wird eine Skolemkonstante eingeführt und die entstehende Formel ist trotzdem in bereinigter Pränexform. Dass da eine Konstante drinn ist, ist wirklich völlig in Ordnung!
Konstanten müssen nicht gebunden werden, können sie auch gar nicht!! Eine Konstante wird von einer Interpretation auf einen Wert des Universums abgebildet und das ist es dann auch schon. Kein Quantor oder ähnliches.
(Du meinst Übung 62 statt Seite 62 glaube ich.)
Cheers,
Frank
Edit: Igitt. Bis eben war das Posting ohne Smilie, das geht ja nun aber wirklich nicht