Was muss für die Skolemfuntion gegeben sein ?

Muss sie bereinigt sein ?
Muss sie zwangsweise in BPF vorliegen ?

Eine Skolemform ist in bereinigter Pränexform und zusätzlich kommen nur Allquantoren und keine Existenzquantoren mehr in der Formel vor.
Ein Existenzquantor wird durch eine Skolemfunktion oder Skolemkonstante ersetzt, deren Argumente durch voranstehende Allquantoren festgelegt sind.

z.B.
AwExAyEz P(w,x,y,z)

Skolemisierung:
AwAy P(w,s1(w),y,s2(w,y))

Grüße,
Stefan

Eine Frage noch zu der BPF: Dort dürfen doch keine freien Variablen mehr auftauchen oder ?
Wenn dies der Fall ist muss ich einen Existenzquantor an den Anfang schreiben der die freie Variable bindet.
Ist das korrekt ?

soweit ich weiss muss eine BPF nicht geschlossen sein, darf also frei variablen enthalten. skolemform dagegen muss geschlossen sein, man muss also alle freien variablen mit existenzquantoren binden.

soweit ich weiss muss eine BPF nicht geschlossen sein, darf also frei variablen enthalten.

Nein. Bereinigt heisst doch gerade, dass keine freien Variablen vorkommen!

wenn ich das genau nachlese, dann heißt bereinigt lediglich,
dass keine variable sowohl frei als auch gebunden vorkommt,

Bei der Skolemisierung wird eine freie Variable genau wie eine Variable mit Existenzquantor von größtem Skopus behandelt und somit durch eine Skolemkonstante ersetzt.

nein! bereinigt heisst, dass eine variable in F nicht sowhl gebunden als auch frei vorkommt (Folie 10-8).

Folie 10-22: Eine Formel ist in Skolemform, wenn sie in BNF und geschlossen ist, und keine Existenzquantoren enthaelt.

Bei der Skolemisierung wird eine freie Variable genau wie eine Variable mit Existenzquantor von größtem Skopus behandelt und somit durch eine Skolemkonstante ersetzt.

klingt wie die fehlende defintion und ist ja praktisch auch so,
aber steht das auch irgendwo? wär schön

Folie 10-22: Eine Formel ist in Skolemform, wenn sie in BNF und geschlossen ist, und keine Existenzquantoren enthaelt.

auch schön, und sowas fehlt im skript des vorjahres..

oehm… ja, stimmt…

(ist ja schon fast wie bei Dumpfbacke… ich lern F2 und vergess F1…)

GOLF rueckwaerts heisst FLOG :-)