enigmista

User info:

Registered: Jun 2004
Posts: 6 (0.00 al dì)
Location:
Corso:
Anno:
Time Online: 1:31:41 [...]
Status: Offline

Post actions:

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

recoil

dsy adminz

User info:

Registered: Mar 2002
Posts: 4454 (0.51 al dì)
Location: Milano / Erba
Corso: TICOM
Anno: laureato
Time Online: 61 Days, 16:17:45 [...]
Status: Offline

Post actions:

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

enigmista

User info:

Registered: Jun 2004
Posts: 6 (0.00 al dì)
Location:
Corso:
Anno:
Time Online: 1:31:41 [...]
Status: Offline

Post actions:

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

Bigby

User info:

Registered: Jul 2005
Posts: 12 (0.00 al dì)
Location:
Corso:
Anno:
Time Online: 13:17:04: [...]
Status: Offline

Post actions:

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

Aung SanSuu Kyi

.consigliere.

User info:

Registered: Apr 2005
Posts: 141 (0.02 al dì)
Location: cernusco s/n -- biella
Corso: Info
Anno: 2°
Time Online: 1 Day, 23:16:17 [...]
Status: Offline

Post actions:

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

Aung SanSuu Kyi

.consigliere.

User info:

Registered: Apr 2005
Posts: 141 (0.02 al dì)
Location: cernusco s/n -- biella
Corso: Info
Anno: 2°
Time Online: 1 Day, 23:16:17 [...]
Status: Offline

Post actions:

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