Flavia

Regina degli avatar

User info:

Registered: Sep 2002
Posts: 3228 (0.38 al dì)
Location: Bergamo
Corso: TI.COM
Anno: Finito! :D
Time Online: 25 Days, 9:12:10 [...]
Status: Offline

Post actions:

Veramente no! Almeno, all'esame di Gennaio era circa la metà, nel mio esame è stato addirittura di più!
Cioè nel senso, mi aspettavo che ad esempio chiedesse tutti i passaggi dell'esercizio, invece me ne ha chiesto uno e basta, poi la definizione di superposition left e una o due altre cose di teoria. Poi non so se si sia preso bene vedendo che la sua parte la sapevo bene, ed è passato alla parte di Ranise chiedendomi praticamente tutto! Universo di Herbrand, teorema di Herbrand, base di Herbran e come funziona il tutto, poi il perchè si poteva passare ad algoritmi per la semplice soddisfacibilità booleana, come funziona l'algoritmo tipo e quali sono i miglioramenti apportati dalla DPLL! Praticamente tutto tranne la prima parte sulla memoria!

Comunque anche se non vi chiederà tante cose sulle parte di Ranise, non sottovalutatela mi raccomando...soprattutto se capitate con Ranise! In genere comunque le cose da avere chiare in mente sono quelle che ho scritto sopra e che mi ha chiesto, insomma, avere chiaro il quadro generale di come funziona il tutto!

__________________
I ragazzi che si amano si baciano in piedi contro le porte della notte, e la gente che passa li punta con il dito, ma i ragazzi che si amano non ci sono per nessuno ed è la loro ombra soltanto che trema nella notte.
Stimolando la rabbia dei passanti, la loro rabbia il loro disprezzo le risa la loro invidia.
I ragazzi che si amano non ci sono per nessuno.
Essi sono altrove, molto più lontano della notte, molto più in alto del giorno, nell'abbagliante splendore del loro amore.

ripe

- up in the mountains -

User info:

Registered: Jun 2002
Posts: 9469 (1.10 al dì)
Location: Cinisellooo
Corso: TICO TICO
Anno: Primo
Time Online: 61 Days, 2:33:39 [...]
Status: Offline

Post actions:

Grazie, in pratica sono morto...

__________________
«And if you ever smell christian blood up in the mountains, then get your axe and chop them down!»

Cr34t|v3

User info:

Registered: Jun 2002
Posts: 535 (0.06 al dì)
Location: Milano
Corso: oUt
Anno: 0
Time Online: 9 Days, 22:07:13 [...]
Status: Offline

Post actions:

Se qualcuno potesse aiutarmi.. con questo esempio..
ho il seguente output di spass e mi trovo a voler eseguire a mano la SPR instruzione 538..

8[0:Inp] || -> quotient(U,V,divide(U,V))*.
534[0:Res:399.1,16.0] || less_equal(divide(U,zero),V) -> equal(divide(divide(U,V),zero),zero)**.
...
538[0:SpR:534.1,8.0] || less_equal(divide(U,zero),V) -> quotient(divide(U,V),zero,zero)*.

quindi ...
less_equal(divide(U,zero),V) -> equal(divide(divide(U,V),zero),zero)** -> quotient(U,V,divide(U,V))*
-----------------------------------------------------------------------------------------------------------------------------------


nelle dispenze non c'è un esempio di come questa venga fatta con l'output di spass..

devo interpretare l' equal come un segno di ugualianza = ?

e quindi :
->equal(divide(divide(U,V),zero),zero)**
diventerebbe
->divide(divide(U,V),zero)=zero

spero che qualcuno possa chiarirmi questa mia incomprensione..

__________________
Debian rules
Linux User #305560

cerchi una casa in affito x le tue vacanze? Casa Vacanze Sicilia http://www.marsala.sicilia.it

ripe

- up in the mountains -

User info:

Registered: Jun 2002
Posts: 9469 (1.10 al dì)
Location: Cinisellooo
Corso: TICO TICO
Anno: Primo
Time Online: 61 Days, 2:33:39 [...]
Status: Offline

Post actions:

Certo, equal è il segno =, e devi ragionare di conseguenza...

__________________
«And if you ever smell christian blood up in the mountains, then get your axe and chop them down!»