.dsy:it. (http://www.dsy.it/forum/)
- Logica matematica (http://www.dsy.it/forum/forumdisplay.php?forumid=246)
-- [argomenti] Esame... (http://www.dsy.it/forum/showthread.php?threadid=23965)

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.

Grazie, in pratica sono morto...

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

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

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!»