www.vorhilfe.de
Vorhilfe

Kostenlose Kommunikationsplattform für gegenseitige Hilfestellungen.
Hallo Gast!einloggen | registrieren ]
Startseite · Forum · Wissen · Kurse · Mitglieder · Team · Impressum
Forenbaum
^ Forenbaum
Status Vorhilfe
  Status Geisteswiss.
    Status Erdkunde
    Status Geschichte
    Status Jura
    Status Musik/Kunst
    Status Pädagogik
    Status Philosophie
    Status Politik/Wirtschaft
    Status Psychologie
    Status Religion
    Status Sozialwissenschaften
  Status Informatik
    Status Schule
    Status Hochschule
    Status Info-Training
    Status Wettbewerbe
    Status Praxis
    Status Internes IR
  Status Ingenieurwiss.
    Status Bauingenieurwesen
    Status Elektrotechnik
    Status Maschinenbau
    Status Materialwissenschaft
    Status Regelungstechnik
    Status Signaltheorie
    Status Sonstiges
    Status Technik
  Status Mathe
    Status Schulmathe
    Status Hochschulmathe
    Status Mathe-Vorkurse
    Status Mathe-Software
  Status Naturwiss.
    Status Astronomie
    Status Biologie
    Status Chemie
    Status Geowissenschaften
    Status Medizin
    Status Physik
    Status Sport
  Status Sonstiges / Diverses
  Status Sprachen
    Status Deutsch
    Status Englisch
    Status Französisch
    Status Griechisch
    Status Latein
    Status Russisch
    Status Spanisch
    Status Vorkurse
    Status Sonstiges (Sprachen)
  Status Neuerdings
  Status Internes VH
    Status Café VH
    Status Verbesserungen
    Status Benutzerbetreuung
    Status Plenum
    Status Datenbank-Forum
    Status Test-Forum
    Status Fragwürdige Inhalte
    Status VH e.V.

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
Dt. Schulen im Ausland: Mathe-Seiten:

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