Klauselmenge für Resolution < Prädikatenlogik < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
Status: |
(Frage) überfällig | Datum: | 03:23 So 06.02.2011 | Autor: | someone |
Aufgabe | Gegeben seien folgende Axiome:
[mm] \forall [/mm] x [mm] \forall [/mm] y (P(x,y) [mm] \wedge [/mm] Q(f(x))) [mm] \Rightarrow [/mm] (R(g(y,x)) [mm] \wedge [/mm] R(g(x,y)))
[mm] \forall [/mm] x [mm] \forall [/mm] y R(g(x,y)) [mm] \Rightarrow \exists [/mm] z S(f(x), g(y,z))
und die Behauptung:
[mm] \forall [/mm] x [mm] \forall [/mm] y [mm] \exists [/mm] z [mm] \exists [/mm] v (P(x,y) [mm] \wedge [/mm] Q(z)) [mm] \Rightarrow [/mm] (R(g(y,x)) [mm] \wedge [/mm] S(z, v))
Bilden Sie die initiale unerfüllbare Klauselmenge (die Ausgangspunkt für einen Resolutionsbeweis sein könnte). |
Hallo,
bei dieser Aufgabe bin ich mir unsicher hinsichtlich des Geltungsbreiches der Quantoren und hoffe, dass mir jemand etwas Licht in's Dunkel bringen kann.
Konkret bin ich mir unsicher beim ersten Axiom und der Behauptung, da dort auf die ersten Quantoren eine Klammer folgt, die nicht den gesamten Ausdruck umfasst.
Zur Vereinfachung meiner Frage sei [mm] \forall [/mm] x (P(x)) [mm] \Rightarrow [/mm] (R(x)). Da dem Allquantor für x direkt eine Klammer folgt, die noch vor der Implikation schließt, würde ich davon ausgehen, dass das x in P an den Allquantor gebunden ist, und das x in R hingegen eine ungebundene Variable ist. Liege ich damit korrekt oder ist das x in R auch an den Allquantor gebunden?
Beste Grüße
ps: Ich habe diese Frage in keinem Forum auf anderen Internetseiten gestellt.
|
|
|
|
Status: |
(Frage) überfällig | Datum: | 18:46 So 06.02.2011 | Autor: | someone |
Aufgabe | Gegeben seien folgende Axiome:
[mm] {\forall x \forall y (P(x,y) \wedge Q(f(x))) \Rightarrow (R(g(y,x)) \wedge R(g(x,y)))}
[/mm]
[mm] {\forall x \forall y R(g(x,y)) \Rightarrow \exists z S(f(x), g(y,z))}
[/mm]
und die Behauptung:
[mm] {\forall x \forall y \exists z \exists v (P(x,y) \wedge Q(z)) \Rightarrow (R(g(y,x)) \wedge S(z, v))}
[/mm]
Bilden Sie die initiale unerfüllbare Klauselmenge (die Ausgangspunkt für einen Resolutionsbeweis sein könnte). |
Hallo,
hier noch meine Lösungsansätze für diese Aufgabe (a, b, c seien Konstanten u, v, w, x, y, z seien Variablen):
Erstes Axiom
1. Allquantoren gelten nur für die direkt folgende Klammerung
a. Umbenennung der ungebundenen Variablen
[mm] {\forall x \forall y (P(x, y) \wedge Q(f(x))) \Rightarrow (R(g(w, v)) \wedge R(g(v, w)))}
[/mm]
b) Bindung der ungebundenen Variablen
[mm] {\forall x \forall y (P(x, y) \wedge Q(f(x))) \Rightarrow \exists v \exists w (R(g(w, v)) \wedge R(g(v, w)))}
[/mm]
c) Überführung in Pränexform
[mm] {\forall x \forall y \exists v \exists w (P(x, y) \wedge Q(f(x))) \Rightarrow (R(g(w, v)) \wedge R(g(v, w)))}
[/mm]
d) Überführung in Skolemform
[mm] {\forall x \forall y (P(x, y) \wedge Q(f(x))) \Rightarrow (R(g(i(x, y), h(x, y))) \wedge R(g(h(x, y), i(x, y))))}
[/mm]
e) Eliminieren der Implikation
[mm] {\neg (P(x, y) \wedge Q(f(x))) \vee (R(g(i(x, y),h(x, y))) \wedge R(g(h(x, y),i(x, y))))}
[/mm]
f) Negierung auflösen
[mm] {(\neg P(x, y) \vee \neg Q(f(x))) \vee (R(g(i(x, y), h(x, y))) \wedge R(g(h(x, y), i(x, y))))}
[/mm]
g) Anwendung von Distributivgesetzen
[mm] {(\neg P(x, y) \vee \neg Q(f(x)) \vee R(g(i(x, y), h(x,y)))) \wedge (\neg P(x, y) \vee \neg Q(f(x)) \vee R(g(h(x, y), i(x, y))))}
[/mm]
[mm] \{\{\neg P(x, y), \neg Q(f(x)), R(g(i(x, y), h(x, y)))\}, \{\neg P(x, y), \neg Q(f(x)), R(g(h(x, y), i(x, y)))\}\}
[/mm]
2. Allquantoren gelten für den gesamten Ausdruck
a) Eliminieren der Implikation
[mm] {\neg (P(x,y) \wedge Q(f(x))) \vee (R(g(y,x)) \wedge R(g(x,y)))}
[/mm]
b) Negierung auflösen
[mm] {(\neg P(x,y) \vee \neg Q(f(x))) \vee (R(g(y,x)) \wedge R(g(x,y)))}
[/mm]
c) Anwendung von Distributivgesetzen
[mm] {(\neg P(x,y) \vee \neg Q(f(x)) \vee R(g(y,x))) \wedge (\neg P(x,y) \vee \neg Q(f(x)) \vee R(g(x,y)))}
[/mm]
[mm] {\{\{\neg P(x,y), \neg Q(f(x)), R(g(y,x))\}, \{\neg P(x,y), \neg Q(f(x)), R(g(x,y))\}\}}
[/mm]
Zweites Axiom
a) Überführung in Pränexform
[mm] {\forall x \forall y \exists z R(g(x, y)) \Rightarrow S(f(x), g(y, z))}
[/mm]
b) Überführung in Skolemform
[mm] {\forall x \forall y R(g(x, y)) \Rightarrow S(f(x), g(y, h(x, y)))}
[/mm]
c) Eliminieren der Implikation
[mm] {\neg R(g(x, y)) \vee S(f(x), g(y, h(x, y)))}
[/mm]
[mm] {\{\{\neg R(g(x, y)), S(f(x), g(y, h(x, y)))\}\}}
[/mm]
Behauptung
1. Allquantoren gelten nur für die direkt folgende Klammerung
Siehe unten.
2. Allquantoren gelten für den gesamten Ausdruck
a) Negieren der Behauptung
[mm] {\neg (\forall x \forall y \exists z \exists v (P(x,y) \wedge Q(z)) \Rightarrow (R(g(y,x)) \wedge S(z, v)))}
[/mm]
b) Negierung Auflösen bzw. Überführung in Pränexform
[mm] {\exists x \exists y \forall z \forall v \neg((P(x,y) \wedge Q(z)) \Rightarrow (R(g(y,x)) \wedge S(z, v)))}
[/mm]
c) Überführung in Skolemform
[mm] {\forall z \forall v \neg((P(a, b) \wedge Q(z)) \Rightarrow (R(g(b, a)) \wedge S(z, v)))}
[/mm]
d) Eliminieren der Implikation
[mm] {\neg (\neg (P(a, b) \wedge Q(z)) \vee (R(g(b, a)) \wedge S(z, v)))}
[/mm]
e) Negierungen Auflösen
[mm] {\neg (\neg (P(a, b) \wedge Q(z)) \vee (R(g(b, a)) \wedge S(z, v)))}
[/mm]
[mm](P(a, b) \wedge Q(z)) \wedge \neg (R(g(b, a)) \wedge S(z, v))[/mm]
[mm](P(a, b) \wedge Q(z)) \wedge (\neg R(g(b, a)) \vee \neg S(z, v))[/mm]
f) Anwendung von Assoziativgesetzen
[mm]P(a, b) \wedge Q(z) \wedge (\neg R(g(b, a)) \vee \neg S(z, v))[/mm]
[mm] {\{\{P(a, b)\}, \{Q(z)\}, \{\neg R(g(b, a)), \neg S(z, v)\}\}}
[/mm]
Die geforderte Klauselmenge würde sich dann ergeben aus [mm]erstes Axiom \cup zweites Axiom \cup \neg Behauptung[/mm] bzw. durch Vereinigung der hier abgeleiteten Klauselmengen.
Zu meiner ersten Frage bezüglich des Skopus der Quantoren ist mir nun in der Behauptung aufgefallen, dass dort zu Begin der Existenzquantor für v verwendet wird, v jedoch erst nach der fraglichen Klammer verwendet wird. Ich würde daher davon ausgehen, dass hier die Quantoren in dem ersten Axiom und der Behauptung für den gesamten Ausdruck gültig sind. Also die Schritte 1.a-g für das erste Axiom nicht korrekt sind. Damit wäre die vollständige Klauselmenge: [mm]\{\{\neg P(x,y), \neg Q(f(x)), R(g(y,x))\}, \{\neg P(x,y), \neg Q(f(x)), R(g(x,y))\}, \{\neg R(g(x, y)), S(f(x), g(y, h(x, y)))\}, \{P(a, b)\}, \{Q(z)\}, \{\neg R(g(b, a)), \neg S(z, v)\}\}[/mm].
Kann mir vielleicht jemand sagen, ob meine Annahmen und die Lösungsansätze (ohne 1. a-g für das erste Axiom) korrekt sind?
Beste Grüße
ps: Ich habe diese Frage in keinem Forum auf anderen Internetseiten gestellt
|
|
|
|
|
Status: |
(Mitteilung) Reaktion unnötig | Datum: | 19:20 Do 10.02.2011 | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
|
Status: |
(Mitteilung) Reaktion unnötig | Datum: | 04:20 Mi 09.02.2011 | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
|
> Gegeben seien folgende Axiome:
>
> [mm]\forall[/mm] x [mm]\forall[/mm] y (P(x,y) [mm]\wedge[/mm] Q(f(x))) [mm]\Rightarrow[/mm]
> (R(g(y,x)) [mm]\wedge[/mm] R(g(x,y)))
> [mm]\forall[/mm] x [mm]\forall[/mm] y R(g(x,y)) [mm]\Rightarrow \exists[/mm] z
> S(f(x), g(y,z))
>
> und die Behauptung:
>
> [mm] $\forall{x}\ \forall{y}\ \exists{z}\exists{v} [/mm] (P(x,y)\ [mm] \wedge\ Q(z))\Rightarrow\ (R(g(y,x))\wedgeS(z, [/mm] v))$
>
> Bilden Sie die initiale unerfüllbare Klauselmenge (die
> Ausgangspunkt für einen Resolutionsbeweis sein könnte).
> Hallo,
>
> bei dieser Aufgabe bin ich mir unsicher hinsichtlich des
> Geltungsbreiches der Quantoren und hoffe, dass mir jemand
> etwas Licht in's Dunkel bringen kann.
>
> Konkret bin ich mir unsicher beim ersten Axiom und der
> Behauptung, da dort auf die ersten Quantoren eine Klammer
> folgt, die nicht den gesamten Ausdruck umfasst.
>
> Zur Vereinfachung meiner Frage sei
> [mm]\forall[/mm] x (P(x)) [mm]\Rightarrow[/mm] (R(x))
> Da dem Allquantor für x direkt eine
> Klammer folgt, die noch vor der Implikation schließt,
> würde ich davon ausgehen, dass das x in P an den
> Allquantor gebunden ist, und das x in R hingegen eine
> ungebundene Variable ist. Liege ich damit korrekt oder ist
> das x in R auch an den Allquantor gebunden?
>
> Beste Grüße
Hallo Jemand,
mir war bis jetzt nicht einmal der Ausdruck "Skopus" eines
Quantors bekannt - allerdings habe ich dann sofort gemerkt,
dass dies dasselbe bedeuten muss wie das englische "scope",
also etwa "Reichweite", "Anwendungsbereich".
In Wikipedia steht:
In der Logik versteht man unter dem Bereich, der Reichweite
oder dem Skopus (engl. scope „Bereich“, von lat. scopus „Ziel“)
eines Quantors die kürzeste Formel, die diesem Quantor unmit-
telbar folgt.
So interpretiert liegst du richtig mit der Annahme, dass sich
der Allquantor nur auf das P(x) bezieht. Allerdings fragt man
sich, was dann das ungebundene x in R(x) überhaupt soll.
Leider wird mit der Beklammerung in derartigen Termen oft
zu locker umgegangen, woraus dann nicht bloß einigermaßen
harmlose "Missverständnisse", sondern wirkliche Fehler
entstehen.
Übrigens:
mit deinen "Lösungsansätzen" in deinem zweiten Beitrag
hast du offensichtlich einen erheblichen Aufwand betrieben.
Es wäre schön, wenn dir darauf noch jemand antworten könnte.
LG Al-Chw.
|
|
|
|