Esperienza di esame
Clicca QUI per vedere il messaggio nel forum |
| Orion |
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 |
| Innanzitutto grazie per aver postato un resoconto sull'esame, ma per quanto riguarda la parte di Ranise cosa ti e' stato chiesto? |
| Flavia |
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) |
| Orion |
| 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. |
|
|
|
