Forma normale di SKOLEM

[slyb]

Ciao
un dubbio sulla trasformazione in forma normale di SKOLEM. Se ho la seguente formula $forallxexistsyA(x,y) -> existsxforallyB(x,y)$
qual è il procedimento corretto? il primo o il secondo?

formula di partenza $forallxexistsyA(x,y) -> existsxforallyB(x,y)$

1) in questa sequenza prima si trasforma in forma congiunta e poi si estraggono i quantificatori
$ not(forallxexistsyA(x,y) )V existsxforallyB(x,y)$
$(existsxforallynotA(x,y) V existsxforallyB(x,y)$
$existsx(forallynotA(x,y) V forallyB(x,y))$
$existsx(forallynotA(x,y) V forallyB(x,y))$
$existsxforalltforally (notA(x,t) V B(x,y))$

2) in questa sequenza prima si portano in testa i quantificatori e poi si trasforma in forma congiunta
ed il risultato è molto diverso da quello dato nel primo procedimento
$forallxexistsy (A(x,y) )-> existstforallwB(t,w)$
$forallxexistsyexiststforallw (A(x,y) )->B(t,w))$
$forallxexistsyexiststforallw(notA(x,y) V B(t,w))$



Grazie mille
B.

[Martino]

[mod="Martino"]I simboli $forall$, $exists$ e $not$ non vengono visualizzati correttamente se li importi da una mappa caratteri. Sei pregato di sostituire il simbolo $forall$ con la parola "forall", il simbolo $exists$ con la parola "exists" e il simbolo $not$ con la parola "not". Clicca su "modifica" nel tuo intervento. Grazie.[/mod]

[Rggb1]

I tuoi passaggi non mi sono molto chiari... Sicuramente va bene trasformare "$alpha ->beta$" in "$not alpha vv beta$", se proprio l'implicazione ti da noia. Ma forse non ho capito qual è il tuo dubbio.

In generale devi trasformare prima il tutto in forma normale prenessa e poi rimuovere i quantificatori esistenziali (ovvero procedere alla skolemizazione).