| |
| Autor |
 Resolution in der Prädikatenlogik |
|
inf
Ehemals Aktiv 
Dabei seit: 02.11.2013
Mitteilungen: 23
 |  Themenstart: 2017-04-28
|
1. Frage
(\not\ \forall\ x\exists\ yP(x,y)) \and\ (\exists\ u\forall\ z P(z,u))
(\exists\ x\forall\ y\not\ P(x,y))\and\ (\exists\ u\forall\ z P(z,u))
\exists\ x\forall\ y\exists\ u\forall\ z P(z,u) \and\ \not\ P(x, y)
Skolemisierung mit c und f(y):
\forall\ y\forall\ z P(z,f(y)) \and\ \not\ P(c,y)
Ich befürchte, dass ich dabei bereits etwas falsch gemacht habe.
Ziel ist eine Resolution. Doch ergibt sich so die Klauselmenge
menge(menge(P(z, f(y))), menge(\not\ P(c,y)))
sodass eine Unifikation wegen f(y) und y nicht möglich ist.
2. Frage
Das Skript sagt, dass eine Unifikation von f(x,b) und f(a,c) nicht möglich ist. Stimmt das? Geht nicht o={x/a, b/c}?
|
 Profil
|
Zwerg_Allwissend
Senior 
Dabei seit: 02.12.2013
Mitteilungen: 327
| Beitrag No.1, eingetragen 2017-04-29
|
\quoteon(2017-04-28 23:10 - inf im Themenstart)
1. Frage
(\not\ \forall\ x\exists\ yP(x,y)) \and\ (\exists\ u\forall\ z P(z,u))
(\exists\ x\forall\ y\not\ P(x,y))\and\ (\exists\ u\forall\ z P(z,u))
\exists\ x\forall\ y\exists\ u\forall\ z P(z,u) \and\ \not\ P(x, y)
Skolemisierung mit c und f(y):
\forall\ y\forall\ z P(z,f(y)) \and\ \not\ P(c,y)
Ich befürchte, dass ich dabei bereits etwas falsch gemacht habe.
Ziel ist eine Resolution. Doch ergibt sich so die Klauselmenge
menge(menge(P(z, f(y))), menge(\not\ P(c,y)))
sodass eine Unifikation wegen f(y) und y nicht möglich ist.
\quoteoff
Richtig vermutet - nach dem 1. Unformungsschritt hat man bereits eine KNF in Prenex NF und kann skolemisieren: {~P(a, y)}, {P(z, b)}.
\quoteon(2017-04-28 23:10 - inf im Themenstart)
2. Frage
Das Skript sagt, dass eine Unifikation von f(x,b) und f(a,c) nicht möglich ist. Stimmt das? Geht nicht o={x/a, b/c}?
\quoteoff
Ich vermute, daß das Skript auch sagt: b ist eine Konstante (und dann ist b/c nicht möglich).
|
Profil
|
inf
Ehemals Aktiv
Dabei seit: 02.11.2013
Mitteilungen: 23
| Beitrag No.2, vom Themenstarter, eingetragen 2017-04-29
|
Danke, deine Antwort hat mir schon weitergeholfen!
\quoteon(2017-04-29 00:24 - Zwerg_Allwissend in Beitrag No. 1)
Richtig vermutet - nach dem 1. Unformungsschritt hat man bereits eine KNF in Prenex NF und kann skolemisieren: {~P(a, y)}, {P(z, b)}.\quoteoff
\quoteoff
"Eine Formel der Prädikatenlogik erster Stufe heißt in Pränexform, wenn sie die Gestalt Q1x1...Qnxn G hat, n≥0, wobei die Qi Quantoren sind und in G kein Quantor vorkommt." (http://www.en.pms.ifi.lmu.de/publications/projektarbeiten/Claudia.Plant_Alije.Ristemi/node32.html)
Das gilt dann aber nur pro Klausel und nicht für die komplette, alle Konjunktionen umfassende Formel.
Meine weiteren Umformungen sollten korrekt sein oder? Warum erhalte ich dann trotzdem eine Klauselmenge, die im Gegensatz zu der nach dem 1. Schritt nicht unifizierbar ist?
\quoteon(2017-04-29 00:24 - Zwerg_Allwissend in Beitrag No. 1)
Ich vermute, daß das Skript auch sagt: b ist eine Konstante (und dann ist b/c nicht möglich).
\quoteoff
Richtig vermutet. Einige Seiten vorher wird eine Konvention festgelegt, die besagt, dass Kleinbuchstanden vom Beginn des Alphabets Konstanten sind, wohingegen solche vom Ende des Alphabets Variablen sind.
|
Profil
|
Zwerg_Allwissend
Senior
Dabei seit: 02.12.2013
Mitteilungen: 327
| Beitrag No.3, eingetragen 2017-04-29
|
\quoteon(2017-04-29 08:13 - inf in Beitrag No. 2)
Meine weiteren Umformungen sollten korrekt sein oder?.
\quoteoff
Nein, sind sie nicht. x und y kommen nicht in P(z, u) vor und u und z nicht in ~P(x, y). Damit kann man die Quantoren verschieben und erhält
Ex x Ex u All y All z ~P(x, y) & P(z, u) .
Ich nehme an, daß es hier um eine Übungsaufgabe geht, in der diese Quantorenverschiebungen behandelt werden. Das müßte eigentlich im Skript stehen. Andernfalls im "Klassiker" des Resolutionsbeweisens
https://www.elsevier.com/books/symbolic-logic-and-mechanical-theorem-proving/chang/978-0-08-091728-3
nachschauen. Steht in jeder Bibliothek und ist vermutlich auch als freier Download im Web erhältlich.
|
Profil
|
inf
Ehemals Aktiv
Dabei seit: 02.11.2013
Mitteilungen: 23
| Beitrag No.4, vom Themenstarter, eingetragen 2017-04-29
|
\quoteon(2017-04-29 14:16 - Zwerg_Allwissend in Beitrag No. 3)
Nein, sind sie nicht. x und y kommen nicht in P(z, u) vor und u und z nicht in ~P(x, y). Damit kann man die Quantoren verschieben und erhält
\quoteoff
Das war mir auch aufgefallen. Im Skript steht allerdings nur, dass aufeinanderfolgende gleiche Quantoren vertauscht werden dürfen.
Dass dein Vorschlag zur richtigen Lösung führt, verstehe ich.
Wir hatten allerdings festgestellt, dass mein Ansatz bis inkl. Zeile 2 korrekt ist. Meinst du mit "Nein, sind sie nicht.", dass meine Umformungen nicht äquivalent, denn das kann ich nicht nachvollziehen?
Ich denke, dass ich im Schritt von Zeile 2 nach 3 die Regel
(\exists\ x F) \and\ G = \exists\ x (F \and\ G)
angewandt haben, sodass es äquivalent sein sollte.
|
Profil
|
inf hat die Antworten auf ihre/seine Frage gesehen.
inf hatte hier bereits selbst das Ok-Häkchen gesetzt. | | inf wird per Mail über neue Antworten informiert. |
|
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2023 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die
Nutzungsbedingungen,
die Distanzierung,
die Datenschutzerklärung und das Impressum.
[Seitenanfang]
|
Home / Seite ohne Frame
Wie unterstütze ich den Matheplaneten mit Geld?
