.dsy:it. (http://www.dsy.it/forum/)
- Logica matematica (http://www.dsy.it/forum/forumdisplay.php?forumid=246)
-- [help] skolemizzazione (http://www.dsy.it/forum/showthread.php?threadid=20584)

skolemizzazione

Ciao

sono nei guai perchè non riesco a trovare niente di utile sulla skolemizzazione
potreste aiutarmi?

avete per caso i fogli da darmi della skolemizzazione che ha dato in aula?
magari avete qualche esercizio perchè io non riesco proprio a capire a cosa serve la skolemizzazione e neanche come si possa svolgere qualche esercizio.

Grazie

ciaoooo

gli esempi che ci sono nelle dispense ti sono chiari?

io per esercitarmi ho usato SPASS con uno dei problemi di esempio, verificando che la mia skolemizzazione fosse uguale a quella del prover

__________________
Sono sempre alla ricerca di curriculum interessanti da segnalare alle società con cui ho contatti. Info in pm

Ciao

A dire il vero non ho trovato sulle dispense normali skolem.
Ho letto da qualche parte che c'è una dispensa con gli esercizi risolti in via celoria
ma non sono riuscito a trovare la dispensa cercando alla cusl e alla cued.
Esiste davvero quella dispensa? dove si trova? c'è anche in rete?

Grazie

ciaoooo

si esiste io me la sono fatta dare direttamente dal professore ma secondo me non la spiega bene,c'è sopra anche l'unificazione e comincia da pagina 12 a pag 24 questa piccola dispensa

quoto Bigby,

la dispensa esiste ma non ti da molto.
cmq la skolemizzazione è più semplice di quello che sembra. Prova a prendere uno dei libri di testo alla isu.

Se riesco (oggi sono un po' preso) ti scrivo i 2 esercizi della dispensa, entro sera

legenda: E= esiste; V= per ogni


Dunque:
la prima cosa:
portare l'enunciato in forma normale premessa, ovvero porti "fuori" tutti i quantificatori sia esistenziali che universali rinominando le eventuali variabili non libere che si trovano "legate" a variabili libere.
es:
P(x) v Vx Q(x) diventa prima
P(x) v Vx1 Q(x1) e poi
Vx1(P(x) v Q(x1)

seconda cosa :
eliminare i quantificatori esistenziali in questo modo: se l'esistenziale è il primo a sinistra, lo elimini sostituendo tutte le istanze della variabile con una costante c.
Se l'esistenziale è preceduto da altri quantificatori universali, lo elimini sostituendo tutte le istanze della variabile con un simbolo di funzione f (nuovo) che ha come argomenti le variabili definite dagli universali
es:
EyVxEx1Vy1 (R(x,y) v S(x1,y1) prendi il primo E
VxEx1Vy1 (R(x,c ) v S(x1,y1) prendi l'altro E
VxVy1 (R(x,c ) v S(f(x) ,y1)

spero sia abbastanza chiaro