www.vorkurse.de
Ein Projekt von vorhilfe.de
Die Online-Kurse der Vorhilfe

E-Learning leicht gemacht.
Hallo Gast!einloggen | registrieren ]
Startseite · Mitglieder · Teams · Forum · Wissen · Kurse · Impressum
Forenbaum
^ Forenbaum
Status Mathe-Vorkurse
  Status Organisatorisches
  Status Schule
    Status Wiederholung Algebra
    Status Einführung Analysis
    Status Einführung Analytisc
    Status VK 21: Mathematik 6.
    Status VK 37: Kurvendiskussionen
    Status VK Abivorbereitungen
  Status Universität
    Status Lerngruppe LinAlg
    Status VK 13 Analysis I FH
    Status Algebra 2006
    Status VK 22: Algebra 2007
    Status GruMiHH 06
    Status VK 58: Algebra 1
    Status VK 59: Lineare Algebra
    Status VK 60: Analysis
    Status Wahrscheinlichkeitst

Gezeigt werden alle Foren bis zur Tiefe 2

Navigation
 Startseite...
 Neuerdings beta neu
 Forum...
 vorwissen...
 vorkurse...
 Werkzeuge...
 Nachhilfevermittlung beta...
 Online-Spiele beta
 Suchen
 Verein...
 Impressum
Das Projekt
Server und Internetanbindung werden durch Spenden finanziert.
Organisiert wird das Projekt von unserem Koordinatorenteam.
Hunderte Mitglieder helfen ehrenamtlich in unseren moderierten Foren.
Anbieter der Seite ist der gemeinnützige Verein "Vorhilfe.de e.V.".
Partnerseiten
Weitere Fächer:

Open Source FunktionenplotterFunkyPlot: Kostenloser und quelloffener Funktionenplotter für Linux und andere Betriebssysteme
Forum "Prädikatenlogik" - Klauselmenge für Resolution
Klauselmenge für Resolution < Prädikatenlogik < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
Ansicht: [ geschachtelt ] | ^ Forum "Prädikatenlogik"  | ^^ Alle Foren  | ^ Forenbaum  | Materialien

Klauselmenge für Resolution: Skopus von Quantoren
Status: (Frage) überfällig Status 
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.

        
Bezug
Klauselmenge für Resolution: Lösungsansätze
Status: (Frage) überfällig Status 
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

Bezug
                
Bezug
Klauselmenge für Resolution: Fälligkeit abgelaufen
Status: (Mitteilung) Reaktion unnötig Status 
Datum: 19:20 Do 10.02.2011
Autor: matux

$MATUXTEXT(ueberfaellige_frage)
Bezug
        
Bezug
Klauselmenge für Resolution: Fälligkeit abgelaufen
Status: (Mitteilung) Reaktion unnötig Status 
Datum: 04:20 Mi 09.02.2011
Autor: matux

$MATUXTEXT(ueberfaellige_frage)
Bezug
        
Bezug
Klauselmenge für Resolution: Mitteilung
Status: (Mitteilung) Reaktion unnötig Status 
Datum: 05:48 Mi 09.02.2011
Autor: Al-Chwarizmi


> 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.  

Bezug
Ansicht: [ geschachtelt ] | ^ Forum "Prädikatenlogik"  | ^^ Alle Foren  | ^ Forenbaum  | Materialien


^ Seitenanfang ^
www.vorkurse.de
[ Startseite | Mitglieder | Teams | Forum | Wissen | Kurse | Impressum ]