Forum by laureateci.it - Risoluzione esercizio

Nome Utente:	Password:
Salva Password
Password Dimenticata?

Tutti i Forum

Magistrale - Primo Anno

Metodi formali dell'Informatica

Risoluzione esercizio

Nuova Discussione

Rispondi

Versione Stampabile

Aggiungi Segnalibro

Autore

Discussione

Ceptive
Nuovo Utente

Regione: Puglia
Prov.: Bari

Inserito il - 27/01/2010 : 10:18:25

Salve ragazzi,

Mi chiedevo se qualche anima pia potrebbe postara la soluzione a questo esercizio:

Dimostrare se è derivabile la seguente formula, in caso contrario costruire un controesempio
perogni X esiste Y A(x,y) -> perogni Y esiste X A(y,x)

Ho visto sul sito del prof la soluzione ma non ho capito bene gli ultimi passaggi..
E poi, come si costruisce il controesempio?

Grazie

Vita e sogni sono fogli di uno stesso libro: leggerli in ordine è vivere, sfogliarli a caso è sognare.
A. Schopenhauer.
http://www.ceptive.it

M]i[K
utente juventino

Regione: Puglia
Prov.: Bari

Inserito il - 27/01/2010 : 11:12:29

Citazione:
Messaggio inserito da Ceptive

Salve ragazzi,

Mi chiedevo se qualche anima pia potrebbe postara la soluzione a questo esercizio:

Dimostrare se è derivabile la seguente formula, in caso contrario costruire un controesempio
perogni X esiste Y A(x,y) -> perogni Y esiste X A(y,x)

Ho visto sul sito del prof la soluzione ma non ho capito bene gli ultimi passaggi..
E poi, come si costruisce il controesempio?

Grazie

Te la posto a parole:

per dimostrare che la formula sia derivabile o meno, devi verificare svolgendo i passaggi che fà il prof (eliminazione connettivi, atomi negati,forna normale prenessa,skolemizzazione,forma di clasusa,ecc.. ), se ottieni una clausola vuota [ ] alla fine dello svolgimento. In tal caso la funzione è derivabile.

Nel caso applicando la risoluzione sulle clausole non ottenessi una clausola vuota [ ], allora devi usare il calcolo dei sequenti di Gentzen, utilizzando il metodo del controesempio, e sfruttando opportunamente le formule per l'eliminazione dei connettivi sul lato SX ed DX della tua formula di partenza(pdf enunciati, slide 70), per poi successivamente sfruttare le regole sui quantificatori di gentzen.

Alla fine della giostra se la formula non risulta essere un assioma, hai trovato un controesempio.

..Se potessi applicare la risoluzione anche alla Juventus, alle mie clausole un pò idiote ed incompetenti C1=Blanc C2=Not Blanc , C3=Secco , C4=Not Secco , otterrei subito una clausola vuota per res[C1,C2] e res[C3,C4], e questo in effetti corrisponderebbe al risultato che stanno ottenendo da 3 anni a questa parte..il vuoto!

Cosi applicherei la logica al calcio

Come si comporta un utente linux quando ha un appuntamento???Ecco qui, ve lo dico io,è semplice:

locate; talk; date; join; wine; cd $HOME; unzip; strip; look; touch; finger; head; mount; fsck; eject; gasp; more; yes; continue; yes; more; fsck; eject; umount; make clean; sleep...

Modificato da - M]i[K in data 27/01/2010 11:21:22