Skolemnormalform < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
Hallo
ich soll eine Formel in die Skolemnormalform bringen. Die Bedingung ist dabei, dass "mindestens eine der verwendeten Skolemfunktionen Stelligkeit Eins hat".
Eigentlich steht in meinem Skript, dass das Ersetzen der existenziell quantifizierten Variablen durch Skolemfunktionen erst ganz zum Schluss zu geschehen hat, aber so wie die Ausgangsformel gebaut ist, sehe ich keine andere Moeglichkeit, diese Ersetzung schon vorher zu machen. Koennt ihr mir sagen, ob das so zulaessig ist:
[mm] \exists [/mm] x [mm] \forall [/mm] y P(x,y) [mm] \to \forall [/mm] x [mm] \exists [/mm] y Q(x,y)
[mm] \Rightarrow
[/mm]
P(x(y),y) [mm] \to [/mm] Q(x,y(x))
[mm] \Rightarrow
[/mm]
P(x(y),y) [mm] \to [/mm] Q(w,z(w))
[mm] \Rightarrow
[/mm]
[mm] \neg [/mm] P(x(y),y) [mm] \vee [/mm] Q(w,z(w))
Also, wie gesagt: Ist das so zulaessig?
Danke und Gruss
Martin
|
|
| |
|
| Status: |
(Antwort) fertig  | | Datum: | 15:44 So 02.12.2007 | | Autor: | koepper |
Hallo Martin,
> ich soll eine Formel in die Skolemnormalform bringen. Die
> Bedingung ist dabei, dass "mindestens eine der verwendeten
> Skolemfunktionen Stelligkeit Eins hat".
> Eigentlich steht in meinem Skript, dass das Ersetzen der
> existenziell quantifizierten Variablen durch
> Skolemfunktionen erst ganz zum Schluss zu geschehen hat,
genau so ist es auch!
> aber so wie die Ausgangsformel gebaut ist, sehe ich keine
> andere Moeglichkeit, diese Ersetzung schon vorher zu
> machen. Koennt ihr mir sagen, ob das so zulaessig ist:
ist es nicht.
Skolemisierung ist keine äquivalente Umformung. Nur die Erfüllbarkeit bleibt dabei erhalten!
> [mm]\exists[/mm] x [mm]\forall[/mm] y P(x,y) [mm]\to \forall[/mm] x [mm]\exists[/mm] y Q(x,y)
Verwende hier: $(A [mm] \to [/mm] B) [mm] \Leftrightarrow (\neg [/mm] A [mm] \vee [/mm] B)$
Dann verwende gebundene Umbenennung, um Variablenkonflikte links und rechts zu vermeiden.
Danach kannst du die Quantoren nach vorne ziehen.
Gruß
Will
|
|
|
| |
|
Hallo!
Kannst du das mal bitte vormachen? Ich weiss naemlich nicht was du mit "gebundener" Umbenennung meinst. Umbenannt hab ich die Variablen ja... Aber wie macht man das "gebunden"??
Danke
Martin
|
|
|
| |
|
| Status: |
(Antwort) fertig | | Datum: | 19:54 So 02.12.2007 | | Autor: | koepper |
Hallo Martin,
"gebundene Umbenennung" bedeutet einfach, daß solche Variablen umbenannt werden, die in Quantoren gebunden sind:
[mm] $\exists [/mm] x [mm] \forall [/mm] y P(x,y) [mm] \to \forall [/mm] x [mm] \exists [/mm] y Q(x,y)$
wird zu
[mm] $\exists [/mm] x [mm] \forall [/mm] y P(x,y) [mm] \to \forall [/mm] a [mm] \exists [/mm] b Q(a,b)$
so einfach....
Gruß
Will
|
|
|
| |
|
Ok, aber wie soll ich dann weitermachen. Nach der von dir vorgeschlagenen Substitution muesste ich doch logischerweise
1) erstmal das [mm] \to [/mm] "wegmachen" (P [mm] \to [/mm] Q [mm] \Rightarrow \neg [/mm] P [mm] \vee [/mm] Q)
2) dann die Quantoren mitsamt Variablen vor die Matrix setzen
Dann komm ich an bei:
[mm] \forall [/mm] x [mm] \forall [/mm] y [mm] \forall [/mm] a [mm] \exists [/mm] b [mm] \neg [/mm] P(x,y) [mm] \vee [/mm] Q(a,b)
Die Substitutionsvorschrift sagt jetzt, dass ich all existenziell quantifizierten Variablen durch eine Funktion der Form f(a,b,c,...) ersetzen muss, wobei a,b,c,... die in der Formel enthaltenen allquantifizierten Variablen sind.
Ich komme also raus bei:
[mm] \neg [/mm] P(x,y) [mm] \vee [/mm] Q(a,b(x,y,a))
Die Aufgabenstellung sagt doch aber, dass mindestens eine der verwendeten Skolemfunktionen Stelligkeit Eins haben muss!
Was kann ich da denn jetzt machen?
Danke und Gruss
Martin
|
|
|
| |
|
| Status: |
(Antwort) fertig | | Datum: | 22:20 So 02.12.2007 | | Autor: | koepper |
Hallo Martin,
> 1) erstmal das [mm]\to[/mm] "wegmachen" (P [mm]\to[/mm] Q [mm]\Rightarrow \neg[/mm] P
> [mm]\vee[/mm] Q)
> 2) dann die Quantoren mitsamt Variablen vor die Matrix
> setzen
>
> Dann komm ich an bei:
>
> [mm]\forall[/mm] x [mm]\forall[/mm] y [mm]\forall[/mm] a [mm]\exists[/mm] b [mm]\neg[/mm] P(x,y) [mm]\vee[/mm] Q(a,b)
Vor y muss ein Existenzquantor stehen, sonst OK.
Die Reihenfolge ist aber nicht ganz zwingend. So gehts auch:
[mm] $\forall [/mm] a [mm] \exists [/mm] b [mm] \forall [/mm] x [mm] \exists [/mm] y [mm] \neg [/mm] P(x,y) [mm] \vee [/mm] Q(a,b)$
(schau mal meinen Quelltext an, mit der Maus über die Formel fahren! Ist doch kürzer und einfacher, oder?)
> Die Substitutionsvorschrift sagt jetzt, dass ich all
> existenziell quantifizierten Variablen durch eine Funktion
> der Form f(a,b,c,...) ersetzen muss, wobei a,b,c,... die in
> der Formel enthaltenen allquantifizierten Variablen sind.
>
> Ich komme also raus bei:
>
> [mm]\neg[/mm] P(x,y) [mm]\vee[/mm] Q(a,b(x,y,a))
>
> Die Aufgabenstellung sagt doch aber, dass mindestens eine
> der verwendeten Skolemfunktionen Stelligkeit Eins haben
> muss!
> Was kann ich da denn jetzt machen?
Du kannst b und y jeweils mit Skolemfunktionen der Stelligkeit 1 eliminieren:
b = f(a) und y = g(x).
Gruß und Gute N8
Will
|
|
|
| |
|
> Vor y muss ein Existenzquantor stehen, sonst OK.
Wie kommt man auf den Existenzquantor?
[mm]\exists x \forall y P(x,y) \to \forall x \exists y Q(x,y)[/mm]
wird doch zu
[mm]\neg \exists x \forall y P(x,y) \vee \forall x \exists y Q(x,y)[/mm]
oder?
> Du kannst b und y jeweils mit Skolemfunktionen der
> Stelligkeit 1 eliminieren:
> b = f(a) und y = g(x).
Mit welcher Regel kann ich das tun? Soweit ich das verstehe muss die Funktion von allen allquantifizierten Variablen abhaengen, oder?
Gruss
Martin
|
|
|
| |
|
| Status: |
(Antwort) fertig | | Datum: | 18:37 Di 04.12.2007 | | Autor: | koepper |
Hallo Martin,
> > Vor y muss ein Existenzquantor stehen, sonst OK.
>
> Wie kommt man auf den Existenzquantor?
>
> [mm]\exists x \forall y P(x,y) \to \forall x \exists y Q(x,y)[/mm]
>
> wird doch zu
>
> [mm]\neg \exists x \forall y P(x,y) \vee \forall x \exists y Q(x,y)[/mm]
>
> oder?
ja, und wenn du die Negierung vor P(x,y) ziehst, drehen sich die Quantoren um. "es gibt" wird zu "für alle" und umgekehrt.
>
> > Du kannst b und y jeweils mit Skolemfunktionen der
> > Stelligkeit 1 eliminieren:
> > b = f(a) und y = g(x).
>
> Mit welcher Regel kann ich das tun? Soweit ich das verstehe
> muss die Funktion von allen allquantifizierten Variablen
> abhaengen, oder?
ja.
Gruß
Will
|
|
|
| |
|
> > Mit welcher Regel kann ich das tun? Soweit ich das verstehe
> > muss die Funktion von allen allquantifizierten Variablen
> > abhaengen, oder?
>
> ja.
Also ich glaube, wir reden aneinander vorbei. Ich erklaer nochmal kurz, was mein Problem ist:
1) Die Aufgabenstellung sagt: "Ermitteln Sie zu dem angegebenen Ausdruck unter Verwendung von Variablenumbenennung ein Skolemnormalform, bei der mindestens eine der verwendeten Skolemfunktionen Stelligkeit Eins hat.
2) Mein Vorschlag war zunaechst, dass ich die Eliminierung der Quantoren direkt ausfuehre (also OHNE vorher die Praenexnormalform zu bilden). Da hast du gesagt, das darf man nicht. Wenn ich jetzt aber die Praenexnormalform zuerst bilde und DANN ERST die Quantoren eliminiere, dann muss ich laut Regel alle existenziell quantifizierten Variablen durch eine Funktion ersetzen, die von ALLEN allquantifizierten Variablen abhaengt. Im konkreten Fall muss ich also die beiden existenziell quantifizierten Variablen durch Funktionen mit Stelligkeit Zwei ersetzen, denn die Formel enthaelt genau 2 allquantifizierte Variablen. Die Aufgabenstellung sagt doch aber, mindestens eine der Skolemfunktionen muss Stelligkeit Eins haben! Verstehst du jetzt mein Problem?
Gruesse
Martin
PS: Ich selbst sehe ja, dass eigentlich nur ein Argument notwendig ist, aber ich muss das Ganze doch irgendwie mit einer syntaktischen Operation plausibel machen.
|
|
|
| |
|
| Status: |
(Antwort) fertig | | Datum: | 23:15 Mi 05.12.2007 | | Autor: | koepper |
Hallo Martin,
> laut Regel alle existenziell quantifizierten Variablen
> durch eine Funktion ersetzen, die von ALLEN
> allquantifizierten Variablen abhaengt. Im konkreten Fall
das ist nicht ganz richtig. Schau doch noch einmal in dein Skript:
Die Skolemfunktion hängt nur von denjenigen Variablen mit Allquantor ab,
die VOR der zu ersetzenden Variablen quantifiziert werden.
Gruß
Will
|
|
|
|
