Hi, leide momentan unter einer Lernblockade……..kann mir die skolemisierung und BNF nicht so richtig klar machen
laut skript ist eine formel bereinigt, falls es keine Variable in f gibt, die in der formel sowohl gebunden als auch frei vorkommt (wie lösst man das?) und falls alle in f unterschiedliche quantorenvariablen aufweisen(wahrscheinlcih erreicht man beide bedingungen nur durch variablensubstitution, oder?)
aber wie substituiert man? z.B. : man hat zweimal die gebundene variable x in einer formel, die jeweils an einen anderen quantor gebunden sind?
Ax P(x) u Ex F(x)
Ax P(x) u Eu F(u)
->bereinigt
AxEu(P(x) uF(u))
BPN
man führt einfach eine 2.variable z.B.y ein,die dann die variable x ersetzt(da,wo x zum zweiten mal gebunden wird)
Ax P(x) u Ey F(y)
Ax P(x) u Eu F(u)
->bereinigt
AxEu(P(x) uF(u))
BPN
AxEu(P(x) v F(u))
Soll BPF lauten und Skolemform müsste lauten
Ax(P(x) v F(g(x)))
g - 1stellig - Skolemfunktion
Ax(P(x) v F(g(x)))
Ist auch Klauselnormalform, für die, die's interessiert.
Ax P(x) u Eu F(u)
->bereinigt
AxEu(P(x) uF(u))
BPN
hm das Eu sollte nach aussen…
Ax P(x) u Eu F(u)
->bereinigt
EuAx(P(x) uF(u))
BPN
warum? weil u nicht von x abhängig ist.. (also richtig ist es wohl auch wenn es nicht aussen ist, aber nicht unbedingt sinnvoll) ich würde die E's zum skolemisieren immer möglichst weit nach aussen packen, dann werden die skolemfunktionen einfacher.
Ax P(x) u Eu F(u)
->bereinigt
AxEu(P(x) uF(u))
BPN
hm das Eu sollte nach aussen…
Ax P(x) u Eu F(u)
->bereinigt
EuAx(P(x) uF(u))
BPN
warum? weil u nicht von x abhängig ist.. (also richtig ist es wohl auch wenn es nicht aussen ist, aber nicht unbedingt sinnvoll) ich würde die E's zum skolemisieren immer möglichst weit nach aussen packen, dann werden die skolemfunktionen einfacher.
EuAx(P(x) uF(u))
Dann wäre Skolemform ja
Ax(P(x) uF(a))
und ist das \equiv zu Ax(P(x) v F(g(x)))
äquivalent zu der Ausgangformel sind Skolemformen nie. BPF ist äquivalent zur Ausgangsfunktion, Skolemformen sind erfüllbarkeits(!)äquivalent
Im Lösungszettel für Aufgabe 12 F1 steht, dass BPF nicht eindeutig sei, da die Reihenfolge, in der man die Quantoren rauszieht variieren kann.
Ich würde meine Hand dafür nicht ins Feuer legen, aber danach müssten sowohl Ax(P(x) u F(a)) und Ax(P(x) u F(g(x))) erfüllbarkeistäquivalent zu Ax P(x) u Ex F(x) sein.
Ich lass mich aber gerne berichtigen wenns jemand genau weiss
ich habe noch eine andere frage zur skolemisierung und pränexform:
muss bei der pränexform oder der skolemisierung das ding nur auch "UND" und "ODER" bestehen oder ist z.b. implikation erlaubt?
was heißt "bereinigte" pränexform?-heißt das, dass man die variblan umbenennt, so dass sie eindeutig zugeordnet werden können?
ich habe noch eine andere frage zur skolemisierung und pränexform:
muss bei der pränexform oder der skolemisierung das ding nur auch "UND" und "ODER" bestehen oder ist z.b. implikation erlaubt?
was heißt "bereinigte" pränexform?-heißt das, dass man die variblan umbenennt, so dass sie eindeutig zugeordnet werden können?
Ich glaube, dass hatten wir schon mal irgendwo.
Du kannst es mit Implikation lassen. Mit & oder v ist vielleicht für manchen einfacher umzuformen.
zu 2. Ja. Es darf keine Variable gebunden UND frei vorkommen
wenn man implikationen und biimplikationen lässt, muss man aber bei quantoren sehr genau aufpassen!
AxP(x)->Q
(nicht)AxP(x) v Q
Ex((nicht)P(x) v Q)
Ex(P(x) -> Q)
A wird hier also zu E, obwohl man das so nicht umbedingt erwarten würde.. bei der biimplikation ists noch schlimmer..
da werden aus einem Quantor dann 2 (einmal E und einmal A)
AxP(x)<->Q
((nicht)AxP(x) v Q) ^ (AxP(x) v (nicht)Q)
(Ex(nicht)P(x) v Q)) ^ (AyP(y) v (nicht)Q)
ExAy((nicht)P(x) v Q)) ^ (P(y) v (nicht)Q))
glaub ich zumindest [img]
http://www.fb18.de/gfx/12.gif[/img]
acg so, ok, würdet ihr also empfehlen, nach der umbennenung implikationen und biimplikationen aufzulösen?
wenn man implikationen und biimplikationen lässt, muss man aber bei quantoren sehr genau aufpassen!
AxP(x)->Q
(nicht)AxP(x) v Q
Ex((nicht)P(x) v Q)
Ex(P(x) -> Q)
A wird hier also zu E, obwohl man das so nicht umbedingt erwarten würde.. bei der biimplikation ists noch schlimmer..
da werden aus einem Quantor dann 2 (einmal E und einmal A)
AxP(x)<->Q
((nicht)AxP(x) v Q) ^ (AxP(x) v (nicht)Q)
(Ex(nicht)P(x) v Q)) ^ (AyP(y) v (nicht)Q)
ExAy((nicht)P(x) v Q)) ^ (P(y) v (nicht)Q))
glaub ich zumindest [img]http://www.fb18.de/gfx/12.gif[/img]
ja, habe ich auch so…
Und Skolemversion wäre dann
Ay((nicht)P(a) v Q)) ^ (P(y) v (nicht)Q))
