Orion

User info:

Registered: Jun 2003
Posts: 87 (0.01 al dì)
Location: Milano
Corso: Informatica
Anno:
Time Online: 18:35:06: [...]
Status: Offline

Post actions:

Dato ora l'esame, vorrei passare un messaggio "positivo" al forum.

Prima di tutto, lanciare sempre SPASS con Sorts=0 -DocProof. EmS e company li da' solo in caso contrario.
Continuando, va bene uno qualunque degli esempi, anche nel caso in cui non fosse proof found, ma dovete essere in grado di spiegare riga per riga tutte le clausole, e di giustificare tutti i passaggi.

A quel punto lui vi chiederà di implementarne uno, tipicamente applicando la regola di RES, o se vi va' di lusso la fattorizzazione destra.

E' facile che vi chieda anche una regola di riduzione.

Nell'insieme l'esame è molto fattibile, avendo l'accortezza di portare l'esercizio stampato e di lanciarlo con quelle opzioni. Lui non fa storie e tende ad aiutare molto sulle definizioni. E' importante sapere TUTTO, magari non bene, ma sapere tutti gli argomenti. Potete non ricordarvi di LPO 1-2-3, ma l'idea generale e almeno una dovreste saperle.

Nell'insieme un bell'esame.

dicane

.illuminato.

User info:

Registered: Oct 2005
Posts: 218 (0.03 al dì)
Location: Milano
Corso: Informatica
Anno: non ricordo :)
Time Online: 4 Days, 8:12:04: [...]
Status: Offline

Post actions:

Innanzitutto grazie per aver postato un resoconto sull'esame, ma per quanto riguarda la parte di Ranise cosa ti e' stato chiesto?

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:

Originally posted by Orion

Prima di tutto, lanciare sempre SPASS con Sorts=0 -DocProof. EmS e company li da' solo in caso contrario.

Anche "Splits=0" (se il programma non è cambiato rispetto allo scorso anno)

__________________
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.

Orion

User info:

Registered: Jun 2003
Posts: 87 (0.01 al dì)
Location: Milano
Corso: Informatica
Anno:
Time Online: 18:35:06: [...]
Status: Offline

Post actions:

Di Ranise chiede la parte finale. Herbrand e il suo insieme, tutta quella roba là che ormai è stata esplusa dal mio povero cranio a mo' di missile. In pratica gli algoritmi per la soddisfacibilità... ma non va troppo in dettaglio, basta che tu conosca i principi. Mi ha fatto provare l'insoddisfacibilità tramite herbrand comunque.